{-# LANGUAGE LambdaCase #-}

-- | Implementation of unification and other core type system building
-- blocks.
module Language.Futhark.TypeChecker.Unify
  ( Constraint (..),
    Usage (..),
    mkUsage,
    mkUsage',
    Level,
    Constraints,
    MonadUnify (..),
    Rigidity (..),
    RigidSource (..),
    BreadCrumbs,
    allDimsFreshInType,
    dimNotes,
    normTypeFully,
    unify,
    unifyMostCommon,
    doUnification,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.Bitraversable
import Data.List qualified as L
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.TypeChecker.Constraints (CtTy (..), Level, Reason (..), TyVarInfo (..))
import Language.Futhark.TypeChecker.Error
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.TySolve qualified as TySolve
import Language.Futhark.TypeChecker.Types

-- | A usage that caused a type constraint.
data Usage = Usage (Maybe T.Text) Loc
  deriving (Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
(Int -> Usage -> ShowS)
-> (Usage -> String) -> ([Usage] -> ShowS) -> Show Usage
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Usage -> ShowS
showsPrec :: Int -> Usage -> ShowS
$cshow :: Usage -> String
show :: Usage -> String
$cshowList :: [Usage] -> ShowS
showList :: [Usage] -> ShowS
Show)

-- | Construct a 'Usage' from a location and a description.
mkUsage :: (Located a) => a -> T.Text -> Usage
mkUsage :: forall a. Located a => a -> Text -> Usage
mkUsage = (Text -> Loc -> Usage) -> Loc -> Text -> Usage
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Text -> Loc -> Usage
Usage (Maybe Text -> Loc -> Usage)
-> (Text -> Maybe Text) -> Text -> Loc -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Maybe Text
forall a. a -> Maybe a
Just) (Loc -> Text -> Usage) -> (a -> Loc) -> a -> Text -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Loc
forall a. Located a => a -> Loc
locOf

-- | Construct a 'Usage' that has just a location, but no particular
-- description.
mkUsage' :: (Located a) => a -> Usage
mkUsage' :: forall a. Located a => a -> Usage
mkUsage' = Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> (a -> Loc) -> a -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Loc
forall a. Located a => a -> Loc
locOf

instance Pretty Usage where
  pretty :: forall ann. Usage -> Doc ann
pretty (Usage Maybe Text
Nothing Loc
loc) = Doc ann
"use at " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall a. Text -> Doc a
textwrap (Loc -> Text
forall a. Located a => a -> Text
locText Loc
loc)
  pretty (Usage (Just Text
s) Loc
loc) = Text -> Doc ann
forall a. Text -> Doc a
textwrap Text
s Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall a. Text -> Doc a
textwrap (Loc -> Text
forall a. Located a => a -> Text
locText Loc
loc)

instance Located Usage where
  locOf :: Usage -> Loc
locOf (Usage Maybe Text
_ Loc
loc) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc

-- | A constraint on a yet-ambiguous size variable, or information
-- about a rigid type parameter or size.
data Constraint
  = ParamSize Loc
  | -- | Is not actually a type, but a term-level size,
    -- possibly already set to something specific.
    Size (Maybe Exp) Usage
  | -- | A size that does not unify with anything -
    -- created from the result of applying a function
    -- whose return size is existential, or otherwise
    -- hiding a size.
    UnknownSize Loc RigidSource
  | -- | A size arising from instantiating a type parameter (of the
    -- given liftedness) with a type whose sizes are not yet known.
    -- In contrast to an ordinary 'Size', unification may determine
    -- that this size is actually existential (unless the type
    -- parameter is unlifted), in which case the constraint is
    -- replaced with 'ExistentialSize'. See Note [Size Inference] in
    -- Language.Futhark.TypeChecker.Terms.
    InstSize Liftedness Usage
  | -- | Another occurrence of the instantiated size denoted by the
    -- given canonical size variable (an 'InstSize'). Kept distinct
    -- from the canonical variable because if the size turns out to
    -- be existential, every occurrence must be a distinct
    -- existential. The integer identifies the occurrence of the
    -- instantiated type parameter that this size is part of; copies
    -- from the same occurrence absorbed from the same source denote
    -- the same existential size.
    CopySize VName Int Usage
  | -- | An instantiated size that unification has determined to
    -- correspond to an existential size, possibly with the variable
    -- it was unified with (used to identify existentials with the
    -- same origin). Each variable constrained by this (or a
    -- 'CopySize' pointing to it) is turned into a rigid size when
    -- the enclosing function application is complete. The second
    -- field, when present, means that a *rigid* unknown size was
    -- absorbed: the existential then stands for a size that is
    -- actually computed at that location, and if it cannot be bound
    -- anywhere, it becomes a rigid unknown size there (see
    -- bindExistentialInsts), subjecting it to the causality check.
    ExistentialSize (Maybe VName) (Maybe Loc) Usage
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show)

instance Located Constraint where
  locOf :: Constraint -> Loc
locOf (ParamSize Loc
loc) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc
  locOf (Size Maybe Exp
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (UnknownSize Loc
loc RigidSource
_) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc
  locOf (InstSize Liftedness
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (CopySize VName
_ Int
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (ExistentialSize Maybe VName
_ Maybe Loc
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage

-- | Mapping from fresh type variables, instantiated from the type
-- schemes of polymorphic functions, to (possibly) specific types as
-- determined on application and the location of that application, or
-- a partial constraint on their type.
type Constraints = M.Map VName (Level, Constraint)

lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst VName
v Constraints
constraints = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
  Just (Size (Just Exp
d) Usage
_) ->
    Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just (Subst StructRetType -> Maybe (Subst StructRetType))
-> Subst StructRetType -> Maybe (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ Exp -> Subst StructRetType
forall t. Exp -> Subst t
ExpSubst (Exp -> Subst StructRetType) -> Exp -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d
  Just (CopySize VName
c Int
_ Usage
_)
    -- If the canonical size has been resolved to an actual size, we
    -- are equal to that size. Otherwise (canonical size still
    -- pending, or existential) we stand apart under our own name.
    | Just (Size (Just Exp
_) Usage
_) <- (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
c Constraints
constraints ->
        VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst VName
c Constraints
constraints
  Maybe Constraint
_ -> Maybe (Subst StructRetType)
forall a. Maybe a
Nothing

-- | The source of a rigid size.
data RigidSource
  = -- | A function argument that is not a constant or variable name.
    RigidArg (Maybe (QualName VName)) T.Text
  | -- | An existential return size.
    RigidRet (Maybe (QualName VName))
  | -- | Similarly to 'RigidRet', but produce by a loop.
    RigidLoop
  | -- | Produced by a complicated slice expression.
    RigidSlice (Maybe Size) T.Text
  | -- | Produced by a complicated range expression.
    RigidRange
  | -- | Mismatch in branches.
    RigidCond StructType StructType
  | -- | Invented during unification.
    RigidUnify
  | -- | A name used in a size went out of scope.
    RigidOutOfScope Loc VName
  deriving (RigidSource -> RigidSource -> Bool
(RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool) -> Eq RigidSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RigidSource -> RigidSource -> Bool
== :: RigidSource -> RigidSource -> Bool
$c/= :: RigidSource -> RigidSource -> Bool
/= :: RigidSource -> RigidSource -> Bool
Eq, Eq RigidSource
Eq RigidSource =>
(RigidSource -> RigidSource -> Ordering)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> RigidSource)
-> (RigidSource -> RigidSource -> RigidSource)
-> Ord RigidSource
RigidSource -> RigidSource -> Bool
RigidSource -> RigidSource -> Ordering
RigidSource -> RigidSource -> RigidSource
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RigidSource -> RigidSource -> Ordering
compare :: RigidSource -> RigidSource -> Ordering
$c< :: RigidSource -> RigidSource -> Bool
< :: RigidSource -> RigidSource -> Bool
$c<= :: RigidSource -> RigidSource -> Bool
<= :: RigidSource -> RigidSource -> Bool
$c> :: RigidSource -> RigidSource -> Bool
> :: RigidSource -> RigidSource -> Bool
$c>= :: RigidSource -> RigidSource -> Bool
>= :: RigidSource -> RigidSource -> Bool
$cmax :: RigidSource -> RigidSource -> RigidSource
max :: RigidSource -> RigidSource -> RigidSource
$cmin :: RigidSource -> RigidSource -> RigidSource
min :: RigidSource -> RigidSource -> RigidSource
Ord, Int -> RigidSource -> ShowS
[RigidSource] -> ShowS
RigidSource -> String
(Int -> RigidSource -> ShowS)
-> (RigidSource -> String)
-> ([RigidSource] -> ShowS)
-> Show RigidSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RigidSource -> ShowS
showsPrec :: Int -> RigidSource -> ShowS
$cshow :: RigidSource -> String
show :: RigidSource -> String
$cshowList :: [RigidSource] -> ShowS
showList :: [RigidSource] -> ShowS
Show)

-- | The ridigity of a size variable.  All rigid sizes are tagged with
-- information about how they were generated.
data Rigidity = Rigid RigidSource | Nonrigid
  deriving (Rigidity -> Rigidity -> Bool
(Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool) -> Eq Rigidity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
/= :: Rigidity -> Rigidity -> Bool
Eq, Eq Rigidity
Eq Rigidity =>
(Rigidity -> Rigidity -> Ordering)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Rigidity)
-> (Rigidity -> Rigidity -> Rigidity)
-> Ord Rigidity
Rigidity -> Rigidity -> Bool
Rigidity -> Rigidity -> Ordering
Rigidity -> Rigidity -> Rigidity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Rigidity -> Rigidity -> Ordering
compare :: Rigidity -> Rigidity -> Ordering
$c< :: Rigidity -> Rigidity -> Bool
< :: Rigidity -> Rigidity -> Bool
$c<= :: Rigidity -> Rigidity -> Bool
<= :: Rigidity -> Rigidity -> Bool
$c> :: Rigidity -> Rigidity -> Bool
> :: Rigidity -> Rigidity -> Bool
$c>= :: Rigidity -> Rigidity -> Bool
>= :: Rigidity -> Rigidity -> Bool
$cmax :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
min :: Rigidity -> Rigidity -> Rigidity
Ord, Int -> Rigidity -> ShowS
[Rigidity] -> ShowS
Rigidity -> String
(Int -> Rigidity -> ShowS)
-> (Rigidity -> String) -> ([Rigidity] -> ShowS) -> Show Rigidity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Rigidity -> ShowS
showsPrec :: Int -> Rigidity -> ShowS
$cshow :: Rigidity -> String
show :: Rigidity -> String
$cshowList :: [Rigidity] -> ShowS
showList :: [Rigidity] -> ShowS
Show)

prettySource :: Loc -> Loc -> RigidSource -> Doc ()
prettySource :: Loc -> Loc -> RigidSource -> Doc ()
prettySource Loc
ctx Loc
loc (RigidRet Maybe (QualName VName)
Nothing) =
  Doc ()
"is unknown size returned by function at"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidRet (Just QualName VName
fname)) =
  Doc ()
"is unknown size returned by"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
fname)
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"at"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidArg Maybe (QualName VName)
fname Text
arg) =
  Doc ()
"is value of argument"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc (ZonkAny 0) -> Doc ()
forall a b. Doc a -> Doc b
shorten (Text -> Doc (ZonkAny 0)
forall a. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
arg))
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"passed to"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall {ann}. Doc ann
fname'
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"at"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  where
    fname' :: Doc ann
fname' = Doc ann
-> (QualName VName -> Doc ann) -> Maybe (QualName VName) -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"function" (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann)
-> (QualName VName -> Doc ann) -> QualName VName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty) Maybe (QualName VName)
fname
prettySource Loc
ctx Loc
loc (RigidSlice Maybe Exp
d Text
slice) =
  Doc ()
"is size produced by slice"
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc (ZonkAny 1) -> Doc ()
forall a b. Doc a -> Doc b
shorten (Text -> Doc (ZonkAny 1)
forall a. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
slice))
    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
forall {ann}. Doc ann
d_desc
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"at"
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  where
    d_desc :: Doc ann
d_desc = case Maybe Exp
d of
      Just Exp
d' -> Doc ann
"of dimension of size " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
d') Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" "
      Maybe Exp
Nothing -> Doc ann
forall a. Monoid a => a
mempty
prettySource Loc
ctx Loc
loc RigidSource
RigidLoop =
  Doc ()
"is unknown size of value returned at" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc RigidSource
RigidRange =
  Doc ()
"is unknown length of range at" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidOutOfScope Loc
boundloc VName
v) =
  Doc ()
"is an unknown size arising from "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" going out of scope at "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Originally bound at "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
boundloc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
_ Loc
_ RigidSource
RigidUnify =
  Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource Loc
ctx Loc
loc (RigidCond StructType
t1 StructType
t2) =
  Doc ()
"is unknown due to conditional expression at "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"One branch returns array of type: "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1)
      Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"The other an array of type:       "
    Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t2)

-- | Retrieve notes describing the purpose or origin of the given
-- t'Size'.  The location is used as the *current* location, for the
-- purpose of reporting relative locations.
dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes
dimNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes a
ctx (Var QualName VName
d Info StructType
_ SrcLoc
_) = do
  c <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) (Constraints -> Maybe (Int, Constraint))
-> m Constraints -> m (Maybe (Int, Constraint))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case c of
    Just (Int
_, UnknownSize Loc
loc RigidSource
rsrc) ->
      Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Notes -> m Notes) -> (Doc () -> Notes) -> Doc () -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Notes
aNote (Doc () -> m Notes) -> Doc () -> m Notes
forall a b. (a -> b) -> a -> b
$
        Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
d) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Loc -> Loc -> RigidSource -> Doc ()
prettySource (a -> Loc
forall a. Located a => a -> Loc
locOf a
ctx) Loc
loc RigidSource
rsrc
    Maybe (Int, Constraint)
_ -> Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty
dimNotes a
_ Exp
_ = Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty

-- | Monads that which to perform unification must implement this type
-- class.
class (Monad m) => MonadUnify m where
  getConstraints :: m Constraints
  putConstraints :: Constraints -> m ()
  modifyConstraints :: (Constraints -> Constraints) -> m ()
  modifyConstraints Constraints -> Constraints
f = do
    x <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
    putConstraints $ f x

  newDimVar :: Usage -> Rigidity -> Name -> m VName
  newRigidDim :: (Located a) => a -> RigidSource -> Name -> m VName
  newRigidDim a
loc = Usage -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar (a -> Usage
forall a. Located a => a -> Usage
mkUsage' a
loc) (Rigidity -> Name -> m VName)
-> (RigidSource -> Rigidity) -> RigidSource -> Name -> m VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RigidSource -> Rigidity
Rigid
  newFlexibleDim :: Usage -> Name -> m VName
  newFlexibleDim Usage
usage = Usage -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar Usage
usage Rigidity
Nonrigid

  curLevel :: m Level

  matchError ::
    (Located loc) =>
    loc ->
    Notes ->
    BreadCrumbs ->
    StructType ->
    StructType ->
    m a

  unifyError ::
    (Located loc) =>
    loc ->
    Notes ->
    BreadCrumbs ->
    Doc () ->
    m a

-- | Replace all type variables with their substitution.
normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a
normTypeFully :: forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully a
t = do
  constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  pure $ applySubst (`lookupSubst` constraints) t

rigidConstraint :: Constraint -> Bool
rigidConstraint :: Constraint -> Bool
rigidConstraint ParamSize {} = Bool
True
rigidConstraint UnknownSize {} = Bool
True
rigidConstraint ExistentialSize {} = Bool
True
rigidConstraint Constraint
_ = Bool
False

-- | If the given type variable is nonrigid, what is its level?
isNonRigid :: VName -> Constraints -> Maybe Level
isNonRigid :: VName -> Constraints -> Maybe Int
isNonRigid VName
v Constraints
constraints = do
  (lvl, c) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints
  case c of
    -- A copy is as rigid as its canonical size.
    CopySize VName
c' Int
_ Usage
_ | Just (Int
_, Constraint
c'') <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
c' Constraints
constraints -> do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Constraint -> Bool
rigidConstraint Constraint
c''
      Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl
    Constraint
_ -> do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Constraint -> Bool
rigidConstraint Constraint
c
      Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl

type UnifySizes m =
  BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Exp -> Exp -> m ()

unifyWith ::
  (MonadUnify m) =>
  UnifySizes m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  StructType ->
  StructType ->
  m ()
unifyWith :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage = Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
False
  where
    swap :: Bool -> a -> a -> (a, a)
swap Bool
True a
x a
y = (a
y, a
x)
    swap Bool
False a
x a
y = (a
x, a
y)

    subunify :: Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs StructType
t1' StructType
t2' = do
      constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

      let nonrigid VName
v = VName -> Constraints -> Maybe Int
isNonRigid VName
v Constraints
constraints

          failure = SrcLoc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
matchError (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs StructType
t1' StructType
t2'

          unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Exp
d1) (TypeArgDim Exp
d2) =
            BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs' (Bool -> Exp -> Exp -> (Exp, Exp)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Exp
d1 Exp
d2)
          unifyTypeArg BreadCrumbs
bcs' (TypeArgType StructType
t) (TypeArgType StructType
arg_t) =
            Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
t StructType
arg_t
          unifyTypeArg BreadCrumbs
_ TypeArg Exp
_ TypeArg Exp
_ = m ()
forall {a}. m a
failure

          onDims' BreadCrumbs
bcs' (Exp
d1, Exp
d2) =
            UnifySizes m
onDims
              BreadCrumbs
bcs'
              [VName]
bound
              VName -> Maybe Int
nonrigid
              (TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d1)
              (TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d2)

      -- The types are structurally identical, as this has already
      -- been verified by the unsized type checker - we are here only
      -- to unify their sizes (and check consumption and freshness
      -- for functions). The 'failure' cases can be reached when the
      -- types contain distinct abstract types that the unsized
      -- checking could not distinguish, and serve as a backstop for
      -- anything it may have missed.
      case (t1', t2') of
        (Scalar (Prim PrimType
pt1), Scalar (Prim PrimType
pt2))
          | PrimType
pt1 PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
== PrimType
pt2 -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        ( Scalar (Record Map Name StructType
fs),
          Scalar (Record Map Name StructType
arg_fs)
          )
            | Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs ->
                [(Name, (StructType, StructType))]
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name (StructType, StructType)
-> [(Name, (StructType, StructType))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name (StructType, StructType)
 -> [(Name, (StructType, StructType))])
-> Map Name (StructType, StructType)
-> [(Name, (StructType, StructType))]
forall a b. (a -> b) -> a -> b
$ (StructType -> StructType -> (StructType, StructType))
-> Map Name StructType
-> Map Name StructType
-> Map Name (StructType, StructType)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name StructType
fs Map Name StructType
arg_fs) (((Name, (StructType, StructType)) -> m ()) -> m ())
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Name
f, (StructType
t1, StructType
t2)) ->
                  Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound (Name -> BreadCrumbs
matchingField Name
f BreadCrumbs -> BreadCrumbs -> BreadCrumbs
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs
bcs) StructType
t1 StructType
t2
        ( Scalar (Sum Map Name [StructType]
cs),
          Scalar (Sum Map Name [StructType]
arg_cs)
          )
            | Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs,
              ([StructType] -> Int) -> Map Name [StructType] -> Map Name Int
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [StructType]
cs Map Name Int -> Map Name Int -> Bool
forall a. Eq a => a -> a -> Bool
== ([StructType] -> Int) -> Map Name [StructType] -> Map Name Int
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [StructType]
arg_cs ->
                [(Name, ([StructType], [StructType]))]
-> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name ([StructType], [StructType])
-> [(Name, ([StructType], [StructType]))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name ([StructType], [StructType])
 -> [(Name, ([StructType], [StructType]))])
-> Map Name ([StructType], [StructType])
-> [(Name, ([StructType], [StructType]))]
forall a b. (a -> b) -> a -> b
$ ([StructType] -> [StructType] -> ([StructType], [StructType]))
-> Map Name [StructType]
-> Map Name [StructType]
-> Map Name ([StructType], [StructType])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [StructType]
cs Map Name [StructType]
arg_cs) (((Name, ([StructType], [StructType])) -> m ()) -> m ())
-> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Name
c, ([StructType]
ts1, [StructType]
ts2)) ->
                  (StructType -> StructType -> m ())
-> [StructType] -> [StructType] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound (Name -> BreadCrumbs
matchingConstructor Name
c BreadCrumbs -> BreadCrumbs -> BreadCrumbs
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs
bcs)) [StructType]
ts1 [StructType]
ts2
        ( Scalar (TypeVar NoMode
_ (QualName [VName]
_ VName
tn) [TypeArg Exp]
targs),
          Scalar (TypeVar NoMode
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Exp]
arg_targs)
          )
            | VName
tn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
              [TypeArg Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
targs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
arg_targs -> do
                let bcs' :: BreadCrumbs
bcs' = Doc () -> BreadCrumbs
matching Doc ()
"When matching type arguments." BreadCrumbs -> BreadCrumbs -> BreadCrumbs
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs
bcs
                (TypeArg Exp -> TypeArg Exp -> m ())
-> [TypeArg Exp] -> [TypeArg Exp] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Exp]
targs [TypeArg Exp]
arg_targs
        ( Scalar (Arrow NoMode
_ PName
p1 Diet
d1 StructType
a1 (RetType [VName]
b1_dims TypeBase Exp Freshness
b1)),
          Scalar (Arrow NoMode
_ PName
p2 Diet
d2 StructType
a2 (RetType [VName]
b2_dims TypeBase Exp Freshness
b2))
          )
            | (Diet -> Diet -> Bool) -> (Diet, Diet) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Diet -> Diet -> Bool
forall a. Ord a => a -> a -> Bool
(<) ((Diet, Diet) -> Bool) -> (Diet, Diet) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Diet -> Diet -> (Diet, Diet)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Diet
d1 Diet
d2 -> do
                Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unify-consuming-param" (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
                  Doc ()
"Parameters"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d1 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
a1)
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"and"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d2 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
a2)
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"are incompatible regarding consuming their arguments."
            | (Freshness -> Freshness -> Bool) -> (Freshness, Freshness) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Freshness -> Freshness -> Bool
forall a. Ord a => a -> a -> Bool
(<) ((Freshness, Freshness) -> Bool) -> (Freshness, Freshness) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Freshness -> Freshness -> (Freshness, Freshness)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord (TypeBase Exp Freshness -> Freshness
forall shape. TypeBase shape Freshness -> Freshness
freshness TypeBase Exp Freshness
b2) (TypeBase Exp Freshness -> Freshness
forall shape. TypeBase shape Freshness -> Freshness
freshness TypeBase Exp Freshness
b1) -> do
                Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
                  Doc ()
"Return types"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (TypeBase Exp Freshness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase Exp Freshness -> Doc ann
pretty TypeBase Exp Freshness
b1)
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"and"
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (TypeBase Exp Freshness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase Exp Freshness -> Doc ann
pretty TypeBase Exp Freshness
b2)
                    Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"have incompatible freshness."
            | Bool
otherwise -> do
                -- Introduce the existentials as size variables so they
                -- are subject to unification.  We will remove them again
                -- afterwards.
                let (Constraint
r1, Constraint
r2) =
                      Bool -> Constraint -> Constraint -> (Constraint, Constraint)
forall {a}. Bool -> a -> a -> (a, a)
swap
                        Bool
ord
                        (Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing Loc
forall a. Monoid a => a
mempty)
                        (Loc -> RigidSource -> Constraint
UnknownSize Loc
forall a. Monoid a => a
mempty RigidSource
RigidUnify)
                lvl <- m Int
forall (m :: * -> *). MonadUnify m => m Int
curLevel
                modifyConstraints (M.fromList (map (,(lvl, r1)) b1_dims) <>)
                modifyConstraints (M.fromList (map (,(lvl, r2)) b2_dims) <>)

                let bound' = [VName]
bound [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> (PName -> Maybe VName) -> [PName] -> [VName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PName -> Maybe VName
pname [PName
p1, PName
p2] [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b1_dims [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims
                subunify
                  (not ord)
                  bound
                  (matching "When matching parameter types." <> bcs)
                  a1
                  a2
                subunify
                  ord
                  bound'
                  (matching "When matching return types." <> bcs)
                  (toStruct b1')
                  (toStruct b2')

                -- If a flexible existential size was resolved to a pending
                -- instantiated size, then that size is existential. This is how
                -- a hole absorbs an existential size from a type it is unified
                -- with. See Note [Size Inference] in
                -- Language.Futhark.TypeChecker.Terms.
                constraints_after <- getConstraints
                -- An existential that was already registered as a
                -- rigid unknown size before we made it unifiable
                -- above (e.g. a pending instantiated size bound by
                -- checkApply) stands for a size that is actually
                -- computed somewhere, so absorbing it incurs a
                -- causality obligation.
                let rigidPre VName
d = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
d Constraints
constraints of
                      Just (UnknownSize Loc
dloc RigidSource
_)
                        | Loc
dloc Loc -> Loc -> Bool
forall a. Eq a => a -> a -> Bool
== Loc
forall a. Monoid a => a
mempty -> Loc -> Maybe Loc
forall a. a -> Maybe a
Just (Loc -> Maybe Loc) -> Loc -> Maybe Loc
forall a b. (a -> b) -> a -> b
$ Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
                        | Bool
otherwise -> Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
dloc
                      Maybe Constraint
_ -> Maybe Loc
forall a. Maybe a
Nothing
                    existentialise VName
d VName
v Usage
usage' =
                      (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
                        ((Int, Constraint) -> (Int, Constraint))
-> VName -> Constraints -> Constraints
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Constraint -> Constraint)
-> (Int, Constraint) -> (Int, Constraint)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Constraint -> Constraint)
 -> (Int, Constraint) -> (Int, Constraint))
-> (Constraint -> Constraint)
-> (Int, Constraint)
-> (Int, Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Constraint -> Constraint
forall a b. a -> b -> a
const (Constraint -> Constraint -> Constraint)
-> Constraint -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe VName -> Maybe Loc -> Usage -> Constraint
ExistentialSize (VName -> Maybe VName
forall a. a -> Maybe a
Just VName
d) (VName -> Maybe Loc
rigidPre VName
d) Usage
usage') VName
v
                    absorbExt VName
d
                      | Just (Size (Just Exp
de) Usage
_) <- (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
d Constraints
constraints_after,
                        Var QualName VName
de_v Info StructType
_ SrcLoc
_ <- TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints_after) Exp
de =
                          case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
de_v) Constraints
constraints_after of
                            Just (InstSize Liftedness
l Usage
usage')
                              | Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
Unlifted ->
                                  VName -> VName -> Usage -> m ()
forall {m :: * -> *}.
MonadUnify m =>
VName -> VName -> Usage -> m ()
existentialise VName
d (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
de_v) Usage
usage'
                            Just (CopySize VName
c Int
_ Usage
usage')
                              | Just (InstSize Liftedness
l Usage
_) <- (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
c Constraints
constraints_after,
                                Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
Unlifted ->
                                  VName -> VName -> Usage -> m ()
forall {m :: * -> *}.
MonadUnify m =>
VName -> VName -> Usage -> m ()
existentialise VName
d VName
c Usage
usage'
                            Maybe Constraint
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                      | Bool
otherwise = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                mapM_ absorbExt (b1_dims <> b2_dims)

                -- Delete the size variables we introduced to represent the
                -- existential sizes.
                modifyConstraints $ \Constraints
m -> (Constraints -> VName -> Constraints)
-> Constraints -> [VName] -> Constraints
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ((VName -> Constraints -> Constraints)
-> Constraints -> VName -> Constraints
forall a b c. (a -> b -> c) -> b -> a -> c
flip VName -> Constraints -> Constraints
forall k a. Ord k => k -> Map k a -> Map k a
M.delete) Constraints
m ([VName]
b1_dims [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims)
            where
              (TypeBase Exp Freshness
b1', TypeBase Exp Freshness
b2') =
                -- Replace one parameter name with the other in the
                -- return type, in case of dependent types.  I.e.,
                -- we want type '(n: i32) -> [n]i32' to unify with
                -- type '(x: i32) -> [x]i32'.
                case (PName
p1, PName
p2) of
                  (Named VName
p1', Named VName
p2') ->
                    let f :: VName -> Maybe (Subst t)
f VName
v
                          | VName
v VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
p2' = Subst t -> Maybe (Subst t)
forall a. a -> Maybe a
Just (Subst t -> Maybe (Subst t)) -> Subst t -> Maybe (Subst t)
forall a b. (a -> b) -> a -> b
$ Exp -> Subst t
forall t. Exp -> Subst t
ExpSubst (Exp -> Subst t) -> Exp -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
p1') SrcLoc
forall a. Monoid a => a
mempty
                          | Bool
otherwise = Maybe (Subst t)
forall a. Maybe a
Nothing
                     in (TypeBase Exp Freshness
b1, TypeSubs -> TypeBase Exp Freshness -> TypeBase Exp Freshness
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
f TypeBase Exp Freshness
b2)
                  (PName
_, PName
_) ->
                    (TypeBase Exp Freshness
b1, TypeBase Exp Freshness
b2)

              pname :: PName -> Maybe VName
pname (Named VName
x) = VName -> Maybe VName
forall a. a -> Maybe a
Just VName
x
              pname PName
Unnamed = Maybe VName
forall a. Maybe a
Nothing
        ( Array NoMode
_ (Shape (Exp
t1_d : [Exp]
t1_ds)) ScalarTypeBase Exp NoMode
t1_et,
          Array NoMode
_ (Shape (Exp
t2_d : [Exp]
t2_ds)) ScalarTypeBase Exp NoMode
t2_et
          ) -> do
            BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs (Bool -> Exp -> Exp -> (Exp, Exp)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Exp
t1_d Exp
t2_d)
            Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify
              Bool
ord
              [VName]
bound
              BreadCrumbs
bcs
              (Shape Exp -> StructType -> StructType
forall dim. Shape dim -> TypeBase dim NoMode -> TypeBase dim NoMode
arrayOf ([Exp] -> Shape Exp
forall dim. [dim] -> Shape dim
Shape [Exp]
t1_ds) (ScalarTypeBase Exp NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Exp NoMode
t1_et))
              (Shape Exp -> StructType -> StructType
forall dim. Shape dim -> TypeBase dim NoMode -> TypeBase dim NoMode
arrayOf ([Exp] -> Shape Exp
forall dim. [dim] -> Shape dim
Shape [Exp]
t2_ds) (ScalarTypeBase Exp NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar ScalarTypeBase Exp NoMode
t2_et))
        (StructType, StructType)
_ -> m ()
forall {a}. m a
failure

anyBound :: [VName] -> ExpBase Info VName -> Bool
anyBound :: [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e = (VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (Exp -> FV
freeInExp Exp
e)) [VName]
bound

unifySizes :: (MonadUnify m) => Usage -> UnifySizes m
unifySizes :: forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
e1 Exp
e2
  | Just [(Exp, Exp)]
es <- Exp -> Exp -> Maybe [(Exp, Exp)]
similarExps Exp
e1 Exp
e2 =
      ((Exp, Exp) -> m ()) -> [(Exp, Exp)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ())
-> (Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b. (a -> b) -> a -> b
$ Usage -> UnifySizes m
forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid) [(Exp, Exp)]
es
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid (Var QualName VName
v1 Info StructType
_ SrcLoc
_) Exp
e2
  | Just Int
lvl1 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1),
    Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e2) Bool -> Bool -> Bool
|| (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1 VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
      Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1) Int
lvl1 Exp
e2
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
e1 (Var QualName VName
v2 Info StructType
_ SrcLoc
_)
  | Just Int
lvl2 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2),
    Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e1) Bool -> Bool -> Bool
|| (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2 VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
      Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2) Int
lvl2 Exp
e1
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
_ Exp
e1 Exp
e2 = do
  -- A size arising from a type parameter instantiation may be linked
  -- to sizes bound within the instantiated type itself (reconstructing
  -- a dependent function type), and when it meets any other bound
  -- size (an existential), it is determined to be existential itself,
  -- rather than this being an error. This is the only way we can know
  -- how instantiated sizes depend on binders and existentials. See
  -- Note [Size Inference] in Language.Futhark.TypeChecker.Terms.
  linked <- Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> Exp -> m Bool
forall {m :: * -> *} {f :: * -> *}.
MonadUnify m =>
ExpBase f VName -> Exp -> m Bool
maybeLocalLink Exp
e1 Exp
e2 m (Bool -> Bool) -> m Bool -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> Exp -> m Bool
forall {m :: * -> *} {f :: * -> *}.
MonadUnify m =>
ExpBase f VName -> Exp -> m Bool
maybeLocalLink Exp
e2 Exp
e1
  absorbed <-
    if linked
      then pure True
      else (||) <$> maybeAbsorb e1 e2 <*> maybeAbsorb e2 e1
  unless absorbed $ do
    notes <- (<>) <$> dimNotes usage e1 <*> dimNotes usage e2
    anon1 <- instMeetsAnonymous e1 e2
    anon2 <- instMeetsAnonymous e2 e1
    if anon1 || anon2
      then
        unifyError usage notes bcs $
          "Sizes"
            <+> dquotes (pretty e1)
            <+> "and"
            <+> dquotes (pretty e2)
            <+> "do not match."
            </> textwrap "This is because a type parameter would be instantiated with a type containing anonymous sizes."
      else
        unifyError usage notes bcs $
          "Sizes"
            <+> dquotes (pretty e1)
            <+> "and"
            <+> dquotes (pretty e2)
            <+> "do not match."
  where
    instConstraint :: Map k (a, Constraint) -> k -> Maybe Constraint
instConstraint Map k (a, Constraint)
constraints k
v = do
      c <- (a, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((a, Constraint) -> Constraint)
-> Maybe (a, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> Map k (a, Constraint) -> Maybe (a, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
v Map k (a, Constraint)
constraints
      case c of
        InstSize {} -> Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just Constraint
c
        CopySize {} -> Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just Constraint
c
        ExistentialSize {} -> Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just Constraint
c
        Constraint
_ -> Maybe Constraint
forall a. Maybe a
Nothing
    -- If the absorbed size is a rigid unknown size, then the
    -- existential stands for a size that is actually computed
    -- somewhere, and uses of it are subject to the causality check.
    -- Sizes bound in the type itself (existentials of a declared
    -- type, parameters) carry no such obligation.
    existentialise :: VName -> Exp -> Usage -> m ()
existentialise VName
v Exp
other Usage
usage' = do
      constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
      let rigidLoc VName
w = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
w Constraints
constraints of
            Just (UnknownSize Loc
wloc RigidSource
_)
              | Loc
wloc Loc -> Loc -> Bool
forall a. Eq a => a -> a -> Bool
== Loc
forall a. Monoid a => a
mempty -> Loc -> Maybe Loc
forall a. a -> Maybe a
Just (Loc -> Maybe Loc) -> Loc -> Maybe Loc
forall a b. (a -> b) -> a -> b
$ Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
              | Bool
otherwise -> Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
wloc
            Maybe Constraint
_ -> Maybe Loc
forall a. Maybe a
Nothing
          computed_at =
            [Loc] -> Maybe Loc
forall a. [a] -> Maybe a
listToMaybe ([Loc] -> Maybe Loc) -> [Loc] -> Maybe Loc
forall a b. (a -> b) -> a -> b
$ (VName -> Maybe Loc) -> [VName] -> [Loc]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VName -> Maybe Loc
rigidLoc ([VName] -> [Loc]) -> [VName] -> [Loc]
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> Set VName -> [VName]
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ Exp -> FV
freeInExp Exp
other
      modifyConstraints $ M.adjust (fmap $ const $ ExistentialSize key computed_at usage') v
      where
        key :: Maybe VName
key = case Exp
other of
          Var QualName VName
other_v Info StructType
_ SrcLoc
_ -> VName -> Maybe VName
forall a. a -> Maybe a
Just (VName -> Maybe VName) -> VName -> Maybe VName
forall a b. (a -> b) -> a -> b
$ QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
other_v
          Exp
_ -> Maybe VName
forall a. Maybe a
Nothing
    -- Linking is fine if every bound size mentioned is a binder of
    -- the instantiated type itself (a registered 'ParamSize'), as
    -- instantiated size variables occur exactly once, and binders
    -- are cloned between occurrences of the instantiated type.
    maybeLocalLink :: ExpBase f VName -> Exp -> m Bool
maybeLocalLink (Var QualName VName
v f StructType
_ SrcLoc
_) Exp
other
      | [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
other,
        QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> [VName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
bound = do
          constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
          let mentioned = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) ([VName] -> [VName]) -> [VName] -> [VName]
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> Set VName -> [VName]
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ Exp -> FV
freeInExp Exp
other
              registeredBinder VName
bv = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
bv Constraints
constraints of
                Just (ParamSize Loc
_) -> Bool
True
                Maybe Constraint
_ -> Bool
False
          case instConstraint constraints (qualLeaf v) of
            Just Constraint
c
              | (VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all VName -> Bool
registeredBinder [VName]
mentioned,
                Constraint -> Bool
notExistential Constraint
c -> do
                  (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
                    ((Int, Constraint) -> (Int, Constraint))
-> VName -> Constraints -> Constraints
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Constraint -> Constraint)
-> (Int, Constraint) -> (Int, Constraint)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Constraint -> Constraint)
 -> (Int, Constraint) -> (Int, Constraint))
-> (Constraint -> Constraint)
-> (Int, Constraint)
-> (Int, Constraint)
forall a b. (a -> b) -> a -> b
$ Constraint -> Constraint -> Constraint
forall a b. a -> b -> a
const (Constraint -> Constraint -> Constraint)
-> Constraint -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Exp -> Usage -> Constraint
Size (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
other) Usage
usage) (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v)
                  Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
            Maybe Constraint
_ -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      where
        notExistential :: Constraint -> Bool
notExistential ExistentialSize {} = Bool
False
        notExistential Constraint
_ = Bool
True
    maybeLocalLink ExpBase f VName
_ Exp
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    maybeAbsorb :: ExpBase f VName -> Exp -> m Bool
maybeAbsorb (Var QualName VName
v f StructType
_ SrcLoc
_) Exp
other
      | [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
other,
        QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v VName -> [VName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
bound = do
          constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
          case snd <$> M.lookup (qualLeaf v) constraints of
            Just (InstSize Liftedness
l Usage
usage')
              | Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
Unlifted ->
                  Bool
True Bool -> m () -> m Bool
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VName -> Exp -> Usage -> m ()
forall {m :: * -> *}. MonadUnify m => VName -> Exp -> Usage -> m ()
existentialise (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v) Exp
other Usage
usage'
            Just ExistentialSize {} ->
              Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
            Just (CopySize VName
c Int
_ Usage
usage') ->
              case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
c Constraints
constraints of
                Just (InstSize Liftedness
l Usage
_)
                  | Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
Unlifted -> Bool
True Bool -> m () -> m Bool
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VName -> Exp -> Usage -> m ()
forall {m :: * -> *}. MonadUnify m => VName -> Exp -> Usage -> m ()
existentialise VName
c Exp
other Usage
usage'
                Just ExistentialSize {} -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
                Maybe Constraint
_ -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
            Maybe Constraint
_ -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    maybeAbsorb ExpBase f VName
_ Exp
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    instMeetsAnonymous :: ExpBase f VName -> Exp -> m Bool
instMeetsAnonymous (Var QualName VName
v f StructType
_ SrcLoc
_) Exp
other
      | [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
other = do
          constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
          pure $ isJust $ instConstraint constraints $ qualLeaf v
    instMeetsAnonymous ExpBase f VName
_ Exp
_ = Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- | Unifies two types.
unify :: (MonadUnify m) => Usage -> StructType -> StructType -> m ()
unify :: forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage = UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith (Usage -> UnifySizes m
forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage) Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
forall a. Monoid a => a
mempty

linkVarToDim ::
  (MonadUnify m) =>
  Usage ->
  BreadCrumbs ->
  VName ->
  Level ->
  Exp ->
  m ()
linkVarToDim :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
vn Int
lvl Exp
e = do
  constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

  -- A copy of an instantiated size is equal to its canonical
  -- variable as long as the size is not existential, so links are
  -- expressed in terms of canonical variables: both when the linked
  -- variable is a copy, and when copies occur in the expression
  -- linked to.
  let canonize VName
v = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
        Just (CopySize VName
c Int
_ Usage
_) ->
          Subst t -> Maybe (Subst t)
forall a. a -> Maybe a
Just (Subst t -> Maybe (Subst t)) -> Subst t -> Maybe (Subst t)
forall a b. (a -> b) -> a -> b
$ Exp -> Subst t
forall t. Exp -> Subst t
ExpSubst (Exp -> Subst t) -> Exp -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
c) (SrcLoc -> Exp) -> SrcLoc -> Exp
forall a b. (a -> b) -> a -> b
$ Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage
        Maybe Constraint
_ -> Maybe (Subst t)
forall a. Maybe a
Nothing
      e' = TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
canonize Exp
e

  case snd <$> M.lookup vn constraints of
    Just (CopySize VName
c Int
_ Usage
_)
      | Just (Int
c_lvl, Constraint
_) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
c Constraints
constraints ->
          Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
c Int
c_lvl Exp
e'
    Maybe Constraint
_
      -- Linking a size to itself is a no-op. This can occur when
      -- unifying a canonical size with one of its own copies.
      | Var (QualName [VName]
_ VName
e_v) Info StructType
_ SrcLoc
_ <- Exp
e',
        VName
e_v VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
vn ->
          () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      | Bool
otherwise -> do
          (VName -> m ()) -> Set VName -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Constraints -> VName -> m ()
forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
checkVar Constraints
constraints) (Set VName -> m ()) -> Set VName -> m ()
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ Exp -> FV
freeInExp Exp
e'

          (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Maybe Exp -> Usage -> Constraint
Size (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
e') Usage
usage)
  where
    checkVar :: Constraints -> VName -> m ()
checkVar Constraints
_ VName
dim'
      | VName
vn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
dim' = do
          notes <- Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e
          unifyError usage notes bcs . withIndexLink "occurs-check" $
            "Occurs check: cannot instantiate"
              <+> dquotes (prettyName vn)
              <+> "with"
              <+> dquotes (pretty e)
              <+> "."
    checkVar Constraints
constraints VName
dim'
      | Just (Int
dim_lvl, Constraint
c) <- VName
dim' VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Constraints
constraints,
        Int
dim_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lvl =
          case Constraint
c of
            ParamSize {} -> do
              notes <- Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e
              unifyError usage notes bcs $
                withIndexLink "scope-violation" $
                  "Cannot link size"
                    <+> dquotes (prettyName vn)
                    <+> "to"
                    <+> dquotes (pretty e)
                    <+> "(scope violation)."
                    </> "This is because"
                    <+> dquotes (pretty $ qualName dim')
                    <+> "is not in scope when"
                    <+> dquotes (prettyName vn)
                    <+> "is introduced."
            Constraint
_ -> (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim' (Int
lvl, Constraint
c)
    checkVar Constraints
_ VName
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

newDimOnMismatch ::
  (MonadUnify m) =>
  Loc ->
  StructType ->
  StructType ->
  m (StructType, [VName])
newDimOnMismatch :: forall (m :: * -> *).
MonadUnify m =>
Loc -> StructType -> StructType -> m (StructType, [VName])
newDimOnMismatch Loc
loc StructType
t1 StructType
t2 = do
  (t, seen) <- StateT (Map (Exp, Exp) VName) m StructType
-> Map (Exp, Exp) VName -> m (StructType, Map (Exp, Exp) VName)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (([VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp)
-> StructType
-> StructType
-> StateT (Map (Exp, Exp) VName) m StructType
forall o (m :: * -> *) d1 d2.
(Monoid o, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 o -> TypeBase d2 o -> m (TypeBase d1 o)
matchDims [VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {p}.
(MonadState (Map (Exp, Exp) VName) (t m), MonadTrans t,
 MonadUnify m) =>
p -> Exp -> Exp -> t m Exp
onDims StructType
t1 StructType
t2) Map (Exp, Exp) VName
forall a. Monoid a => a
mempty
  pure (t, M.elems seen)
  where
    r :: RigidSource
r = StructType -> StructType -> RigidSource
RigidCond StructType
t1 StructType
t2
    same :: (Exp, Exp) -> Bool
same (Exp
e1, Exp
e2) =
      Bool -> ([(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (((Exp, Exp) -> Bool) -> [(Exp, Exp)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Exp, Exp) -> Bool
same) (Maybe [(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Maybe [(Exp, Exp)]
similarExps Exp
e1 Exp
e2
    onDims :: p -> Exp -> Exp -> t m Exp
onDims p
_ Exp
d1 Exp
d2
      | (Exp, Exp) -> Bool
same (Exp
d1, Exp
d2) = Exp -> t m Exp
forall a. a -> t m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
d1
      | Bool
otherwise = do
          -- Remember mismatches we have seen before and reuse the
          -- same new size.
          maybe_d <- (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName))
-> (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
forall a b. (a -> b) -> a -> b
$ (Exp, Exp) -> Map (Exp, Exp) VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Exp
d1, Exp
d2)
          case maybe_d of
            Just VName
d -> Exp -> t m Exp
forall a. a -> t m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> t m Exp) -> Exp -> t m Exp
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
d) (SrcLoc -> Exp) -> SrcLoc -> Exp
forall a b. (a -> b) -> a -> b
$ Loc -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Loc
loc
            Maybe VName
Nothing -> do
              d <- m VName -> t m VName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VName -> t m VName) -> m VName -> t m VName
forall a b. (a -> b) -> a -> b
$ Loc -> RigidSource -> Name -> m VName
forall a. Located a => a -> RigidSource -> Name -> m VName
forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim Loc
loc RigidSource
r Name
"differ"
              modify $ M.insert (d1, d2) d
              pure $ sizeFromName (qualName d) $ srclocOf loc

-- | Like unification, but creates new size variables where mismatches
-- occur.  Returns the new dimensions thus created.
unifyMostCommon ::
  (MonadUnify m) =>
  Usage ->
  StructType ->
  StructType ->
  m (StructType, [VName])
unifyMostCommon :: forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m (StructType, [VName])
unifyMostCommon Usage
usage StructType
t1 StructType
t2 = do
  -- Like 'unifySizes', except we do not fail on mismatches - these
  -- are instead turned into fresh existential sizes in
  -- 'newDimOnMismatch'. The most annoying thing is that we have to
  -- replicate scope checking, because we don't want to link if it
  -- would fail.
  constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

  let expFreeVars = FV -> Set VName
fvVars (FV -> Set VName) -> (Exp -> FV) -> Exp -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> FV
freeInExp
      varLevel VName
v = (Int, Constraint) -> Int
forall a b. (a, b) -> a
fst ((Int, Constraint) -> Int) -> Maybe (Int, Constraint) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints

      -- Check that linking to this expression would not fail in linkVarToDim
      -- due to a ParamSize at a level >= the target level. This replicates the
      -- scope check performed by linkVarToDim's checkVar.
      wouldFail Int
lvl VName
v =
        case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
          Just (Int
dim_lvl, ParamSize {}) -> Int
dim_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lvl
          Maybe (Int, Constraint)
_ -> Bool
False

      -- Can we link a variable at the given level to an expression with the
      -- given free variables? FIXME: something her is fishy. Why do we need to
      -- treat ParamSize specially in wouldFail? Why is the level check for the
      -- other variables not enough?
      canLink Int
lvl VName
vn t VName
bound Set VName
fvs =
        (Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 ((VName -> Maybe Int) -> [VName] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VName -> Maybe Int
varLevel ([VName] -> [Int]) -> [VName] -> [Int]
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList Set VName
fvs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lvl
          Bool -> Bool -> Bool
&& Bool -> Bool
not ((VName -> Bool) -> t VName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
fvs) t VName
bound)
          Bool -> Bool -> Bool
&& Bool -> Bool
not ((VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> VName -> Bool
wouldFail Int
lvl) ([VName] -> Bool) -> [VName] -> Bool
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList Set VName
fvs)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (VName
vn VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
fvs)

      onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Exp
e1 Exp
e2
        | Just [(Exp, Exp)]
es <- Exp -> Exp -> Maybe [(Exp, Exp)]
similarExps Exp
e1 Exp
e2 =
            ((Exp, Exp) -> m ()) -> [(Exp, Exp)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ())
-> (Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b. (a -> b) -> a -> b
$ BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Exp -> Exp -> m ()
onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid) [(Exp, Exp)]
es
      onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid (Var QualName VName
v1 Info StructType
_ SrcLoc
_) Exp
e2
        | Just Int
lvl1 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1),
          Int -> VName -> t VName -> Set VName -> Bool
forall {t :: * -> *}.
Foldable t =>
Int -> VName -> t VName -> Set VName -> Bool
canLink Int
lvl1 (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1) t VName
bound (Exp -> Set VName
expFreeVars Exp
e2) =
            Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1) Int
lvl1 Exp
e2
      onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Exp
e1 (Var QualName VName
v2 Info StructType
_ SrcLoc
_)
        | Just Int
lvl2 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2),
          Int -> VName -> t VName -> Set VName -> Bool
forall {t :: * -> *}.
Foldable t =>
Int -> VName -> t VName -> Set VName -> Bool
canLink Int
lvl2 (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2) t VName
bound (Exp -> Set VName
expFreeVars Exp
e1) =
            Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2) Int
lvl2 Exp
e1
      onDims BreadCrumbs
_ t VName
_ VName -> Maybe Int
_ Exp
_ Exp
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  unifyWith onDims usage mempty mempty t1 t2
  t1' <- normTypeFully t1
  t2' <- normTypeFully t2
  newDimOnMismatch (locOf usage) t1' t2'

-- | Replace *all* dimensions with distinct fresh size variables.
allDimsFreshInType ::
  (MonadUnify m) =>
  Usage ->
  Rigidity ->
  Name ->
  TypeBase d o ->
  m (TypeBase Size o, M.Map VName d)
allDimsFreshInType :: forall (m :: * -> *) d o.
MonadUnify m =>
Usage
-> Rigidity
-> Name
-> TypeBase d o
-> m (TypeBase Exp o, Map VName d)
allDimsFreshInType Usage
usage Rigidity
r Name
desc TypeBase d o
t =
  StateT (Map VName d) m (TypeBase Exp o)
-> Map VName d -> m (TypeBase Exp o, Map VName d)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ((d -> StateT (Map VName d) m Exp)
-> (o -> StateT (Map VName d) m o)
-> TypeBase d o
-> StateT (Map VName d) m (TypeBase Exp o)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> TypeBase a b -> f (TypeBase c d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse d -> StateT (Map VName d) m Exp
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {a}.
(MonadTrans t, MonadUnify m, MonadState (Map VName a) (t m)) =>
a -> t m Exp
onDim o -> StateT (Map VName d) m o
forall a. a -> StateT (Map VName d) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase d o
t) Map VName d
forall a. Monoid a => a
mempty
  where
    onDim :: a -> t m Exp
onDim a
d = do
      v <- m VName -> t m VName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VName -> t m VName) -> m VName -> t m VName
forall a b. (a -> b) -> a -> b
$ Usage -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar Usage
usage Rigidity
r Name
desc
      modify $ M.insert v d
      pure $ sizeFromName (qualName v) $ srclocOf usage

-- Simple pure MonadUnify implementation for unification outside of
-- the term checker. The constraints contain only sizes.

type UnifyMState = (Constraints, Int)

newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
  deriving
    ( Applicative UnifyM
Applicative UnifyM =>
(forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a. a -> UnifyM a)
-> Monad UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$creturn :: forall a. a -> UnifyM a
return :: forall a. a -> UnifyM a
Monad,
      (forall a b. (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b. a -> UnifyM b -> UnifyM a) -> Functor UnifyM
forall a b. a -> UnifyM b -> UnifyM a
forall a b. (a -> b) -> UnifyM a -> UnifyM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
fmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
<$ :: forall a b. a -> UnifyM b -> UnifyM a
Functor,
      Functor UnifyM
Functor UnifyM =>
(forall a. a -> UnifyM a)
-> (forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b c.
    (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM a)
-> Applicative UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> UnifyM a
pure :: forall a. a -> UnifyM a
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
liftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
Applicative,
      MonadState UnifyMState,
      MonadError TypeError
    )

instance MonadUnify UnifyM where
  getConstraints :: UnifyM Constraints
getConstraints = (UnifyMState -> Constraints) -> UnifyM Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnifyMState -> Constraints
forall a b. (a, b) -> a
fst
  putConstraints :: Constraints -> UnifyM ()
putConstraints Constraints
x = (UnifyMState -> UnifyMState) -> UnifyM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UnifyMState -> UnifyMState) -> UnifyM ())
-> (UnifyMState -> UnifyMState) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ \(Constraints
_, Int
i) -> (Constraints
x, Int
i)

  newDimVar :: Usage -> Rigidity -> Name -> UnifyM VName
newDimVar Usage
usage Rigidity
rigidity Name
name = do
    (x, i) <- UnifyM UnifyMState
forall s (m :: * -> *). MonadState s m => m s
get
    put (x, i + 1)
    -- Note that the level is 1, so that fresh sizes may be linked to
    -- the rigid parameters, which are at level 0.
    let dim = Name -> Int -> VName
VName (Name -> Int -> Name
mkTypeVarName Name
name Int
i) Int
i
    case rigidity of
      Rigid RigidSource
src ->
        (Constraints -> Constraints) -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
-> (Constraints -> Constraints) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
          VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
1, Loc -> RigidSource -> Constraint
UnknownSize (Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage) RigidSource
src)
      Rigidity
Nonrigid ->
        (Constraints -> Constraints) -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
-> (Constraints -> Constraints) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
          VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
1, Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing Usage
usage)
    pure dim

  curLevel :: UnifyM Int
curLevel = Int -> UnifyM Int
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
1

  unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc ()
doc =
    TypeError -> UnifyM a
forall a. TypeError -> UnifyM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (loc -> Loc
forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (Doc () -> TypeError) -> Doc () -> TypeError
forall a b. (a -> b) -> a -> b
$ Doc ()
doc Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs

  matchError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 =
    TypeError -> UnifyM a
forall a. TypeError -> UnifyM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (loc -> Loc
forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (Doc () -> TypeError) -> Doc () -> TypeError
forall a b. (a -> b) -> a -> b
$ Doc ()
forall {ann}. Doc ann
doc Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs
    where
      doc :: Doc a
doc =
        Doc a
"Types"
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1)
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"and"
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t2)
          Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc a
"do not match."

runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM :: forall a.
[TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams (UnifyM StateT UnifyMState (Except TypeError) a
m) =
  Except TypeError a -> Either TypeError a
forall e a. Except e a -> Either e a
runExcept (Except TypeError a -> Either TypeError a)
-> Except TypeError a -> Either TypeError a
forall a b. (a -> b) -> a -> b
$ StateT UnifyMState (Except TypeError) a
-> UnifyMState -> Except TypeError a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT UnifyMState (Except TypeError) a
m (Constraints
constraints, Int
0)
  where
    constraints :: Constraints
constraints =
      [(VName, (Int, Constraint))] -> Constraints
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, (Int, Constraint))] -> Constraints)
-> [(VName, (Int, Constraint))] -> Constraints
forall a b. (a -> b) -> a -> b
$
        (TypeParam -> Maybe (VName, (Int, Constraint)))
-> [TypeParam] -> [(VName, (Int, Constraint))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe (VName, (Int, Constraint))
forall {a} {a}.
Num a =>
TypeParamBase a -> Maybe (a, (a, Constraint))
nonrigid [TypeParam]
nonrigid_tparams [(VName, (Int, Constraint))]
-> [(VName, (Int, Constraint))] -> [(VName, (Int, Constraint))]
forall a. Semigroup a => a -> a -> a
<> (TypeParam -> Maybe (VName, (Int, Constraint)))
-> [TypeParam] -> [(VName, (Int, Constraint))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe (VName, (Int, Constraint))
forall {a} {a}.
Num a =>
TypeParamBase a -> Maybe (a, (a, Constraint))
rigid [TypeParam]
rigid_tparams
    nonrigid :: TypeParamBase a -> Maybe (a, (a, Constraint))
nonrigid (TypeParamDim a
p SrcLoc
ploc) =
      (a, (a, Constraint)) -> Maybe (a, (a, Constraint))
forall a. a -> Maybe a
Just (a
p, (a
1, Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> Loc -> Usage
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
ploc))
    nonrigid TypeParamType {} = Maybe (a, (a, Constraint))
forall a. Maybe a
Nothing
    rigid :: TypeParamBase a -> Maybe (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
ploc) = (a, (a, Constraint)) -> Maybe (a, (a, Constraint))
forall a. a -> Maybe a
Just (a
p, (a
0, Loc -> Constraint
ParamSize (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
ploc))
    rigid TypeParamType {} = Maybe (a, (a, Constraint))
forall a. Maybe a
Nothing

-- | Check that two types match, instantiating the nonrigid type
-- parameters of the second type as necessary. This is used when
-- matching a value or type in a module against a specification.
--
-- This works in two phases. First the types are checked while
-- disregarding sizes entirely, using the same constraint solver as
-- the unsized type checker. This also determines the instantiation
-- of the nonrigid type parameters, up to sizes. Then the
-- instantiations, given fresh size variables, are substituted into
-- the second type, and the sizes are checked with ordinary
-- (size-only) unification.
doUnification ::
  Loc ->
  [TypeParam] ->
  [TypeParam] ->
  StructType ->
  StructType ->
  Either TypeError ()
doUnification :: Loc
-> [TypeParam]
-> [TypeParam]
-> StructType
-> StructType
-> Either TypeError ()
doUnification Loc
loc [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams StructType
spec_t StructType
t = do
  -- Phase 1: types.
  let typarams :: Map VName (Int, Liftedness, Loc)
typarams =
        [(VName, (Int, Liftedness, Loc))]
-> Map VName (Int, Liftedness, Loc)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
          [ (VName
v, (Int
0, Liftedness
l, SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
tploc))
          | TypeParamType Liftedness
l VName
v SrcLoc
tploc <- [TypeParam]
rigid_tparams
          ]
      tyvars :: Map VName (Int, TyVarInfo d)
tyvars =
        [(VName, (Int, TyVarInfo d))] -> Map VName (Int, TyVarInfo d)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
          [ (VName
v, (Int
1, Loc -> Liftedness -> TyVarInfo d
forall d. Loc -> Liftedness -> TyVarInfo d
TyVarFree (SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
tploc) Liftedness
l))
          | TypeParamType Liftedness
l VName
v SrcLoc
tploc <- [TypeParam]
nonrigid_tparams
          ]
      ct :: CtTy ()
ct = Reason (CtType ()) -> CtType () -> CtType () -> CtTy ()
forall d. Reason (CtType d) -> CtType d -> CtType d -> CtTy d
CtEq (Loc -> Reason (CtType ())
forall t. Loc -> Reason t
Reason Loc
loc) (StructType -> CtType ()
forall {a} {c}. TypeBase a c -> TypeBase () c
unsized StructType
spec_t) (StructType -> CtType ()
forall {a} {c}. TypeBase a c -> TypeBase () c
unsized StructType
t)
  (_, solution) <- [CtTy ()]
-> Map VName (Int, Liftedness, Loc)
-> TyVars ()
-> Either TypeError ([UnconTyVar], Solution)
TySolve.solve [CtTy ()
ct] Map VName (Int, Liftedness, Loc)
typarams TyVars ()
forall {d}. Map VName (Int, TyVarInfo d)
tyvars

  -- The solver does not verify that instantiations respect the
  -- liftedness of the instantiated type parameter, so we check that
  -- here.
  mapM_ (checkLiftedness solution) nonrigid_tparams

  -- Phase 2: sizes.
  runUnifyM rigid_tparams nonrigid_tparams $ do
    -- Give the instantiations of the type parameters fresh size
    -- variables. Crucially, each type parameter is instantiated only
    -- once, so multiple occurrences of the same type parameter will
    -- have the same sizes.
    substs <- fmap (M.fromList . catMaybes) . forM nonrigid_tparams $ \case
      TypeParamType Liftedness
_ VName
v SrcLoc
_
        | Just (Right CtType ()
sol_t) <- VName -> Solution -> Maybe (Either [PrimType] (CtType ()))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Solution
solution -> do
            (sol_t', _) <-
              Usage
-> Rigidity
-> Name
-> CtType ()
-> UnifyM (StructType, Map VName ())
forall (m :: * -> *) d o.
MonadUnify m =>
Usage
-> Rigidity
-> Name
-> TypeBase d o
-> m (TypeBase Exp o, Map VName d)
allDimsFreshInType (Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing Loc
loc) Rigidity
Nonrigid Name
"d" CtType ()
sol_t
            pure $ Just (v, Subst [] $ RetType [] sol_t')
      TypeParam
_ -> Maybe (VName, Subst StructRetType)
-> UnifyM (Maybe (VName, Subst StructRetType))
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (VName, Subst StructRetType)
forall a. Maybe a
Nothing
    unify (Usage Nothing loc) spec_t $ applySubst (`M.lookup` substs) t
  where
    unsized :: TypeBase a c -> TypeBase () c
unsized = (a -> ()) -> TypeBase a c -> TypeBase () c
forall a b c. (a -> b) -> TypeBase a c -> TypeBase b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((a -> ()) -> TypeBase a c -> TypeBase () c)
-> (a -> ()) -> TypeBase a c -> TypeBase () c
forall a b. (a -> b) -> a -> b
$ () -> a -> ()
forall a b. a -> b -> a
const ()

    rigid_liftedness :: Map VName Liftedness
rigid_liftedness =
      [UnconTyVar] -> Map VName Liftedness
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName
v, Liftedness
l) | TypeParamType Liftedness
l VName
v SrcLoc
_ <- [TypeParam]
rigid_tparams]

    checkLiftedness :: Map v (Either a (TypeBase dim o))
-> TypeParamBase v -> Either TypeError ()
checkLiftedness Map v (Either a (TypeBase dim o))
_ (TypeParamDim {}) = () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkLiftedness Map v (Either a (TypeBase dim o))
_ (TypeParamType Liftedness
Lifted v
_ SrcLoc
_) = () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkLiftedness Map v (Either a (TypeBase dim o))
solution (TypeParamType Liftedness
l v
v SrcLoc
_)
      | Just (Right TypeBase dim o
inst_t) <- v
-> Map v (Either a (TypeBase dim o))
-> Maybe (Either a (TypeBase dim o))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Either a (TypeBase dim o))
solution = do
          Bool -> Either TypeError () -> Either TypeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim o -> Bool
forall dim o. TypeBase dim o -> Bool
orderZero TypeBase dim o
inst_t) (Either TypeError () -> Either TypeError ())
-> (Doc () -> Either TypeError ()) -> Doc () -> Either TypeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> (Doc () -> TypeError) -> Doc () -> Either TypeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError ()) -> Doc () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot instantiate type parameter"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (v -> Doc ()
forall a. v -> Doc a
forall v a. IsName v => v -> Doc a
prettyName v
v)
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"with functional type"
              Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (TypeBase dim o -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase dim o -> Doc ann
pretty TypeBase dim o
inst_t)
          case (VName -> Maybe VName) -> [VName] -> [VName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe VName -> Maybe VName
badParam ([VName] -> [VName]) -> [VName] -> [VName]
forall a b. (a -> b) -> a -> b
$ Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> Set VName -> [VName]
forall a b. (a -> b) -> a -> b
$ TypeBase dim o -> Set VName
forall dim o. TypeBase dim o -> Set VName
typeVars TypeBase dim o
inst_t of
            VName
v' : [VName]
_ ->
              TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> (Doc () -> TypeError) -> Doc () -> Either TypeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> Either TypeError ()) -> Doc () -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
                Doc ()
"Cannot instantiate type parameter"
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (v -> Doc ()
forall a. v -> Doc a
forall v a. IsName v => v -> Doc a
prettyName v
v)
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"with type containing lifted type parameter"
                  Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v')
                  Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
            [] -> () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      | Bool
otherwise = () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      where
        badParam :: VName -> Maybe VName
badParam VName
v' = do
          l' <- VName -> Map VName Liftedness -> Maybe Liftedness
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v' Map VName Liftedness
rigid_liftedness
          guard $ case l of
            Liftedness
Unlifted -> Liftedness
l' Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
/= Liftedness
Unlifted
            Liftedness
_ -> Liftedness
l' Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
== Liftedness
Lifted
          Just v'