-- | 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,
    noBreadCrumbs,
    hasNoBreadCrumbs,
    dimNotes,
    zeroOrderType,
    arrayElemType,
    mustHaveConstr,
    mustHaveField,
    mustBeOneOf,
    equalityType,
    normType,
    normTypeFully,
    unify,
    unifyMostCommon,
    doUnification,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Data.List (foldl', intersect)
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.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Types

-- | A piece of information that describes what process the type
-- checker currently performing.  This is used to give better error
-- messages for unification errors.
data BreadCrumb
  = MatchingTypes StructType StructType
  | MatchingFields [Name]
  | MatchingConstructor Name
  | Matching (Doc ())

instance Pretty BreadCrumb where
  pretty :: forall ann. BreadCrumb -> Doc ann
pretty (MatchingTypes StructType
t1 StructType
t2) =
    Doc ann
"When matching type"
      forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
      forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"with"
      forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
  pretty (MatchingFields [Name]
fields) =
    Doc ann
"When matching types of record field"
      forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
fields)
      forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
  pretty (MatchingConstructor Name
c) =
    Doc ann
"When matching types of constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
  pretty (Matching Doc ()
s) =
    forall ann xxx. Doc ann -> Doc xxx
unAnnotate Doc ()
s

-- | Unification failures can occur deep down inside complicated types
-- (consider nested records).  We leave breadcrumbs behind us so we
-- can report the path we took to find the mismatch.
newtype BreadCrumbs = BreadCrumbs [BreadCrumb]

-- | An empty path.
noBreadCrumbs :: BreadCrumbs
noBreadCrumbs :: BreadCrumbs
noBreadCrumbs = [BreadCrumb] -> BreadCrumbs
BreadCrumbs []

-- | Is the path empty?
hasNoBreadCrumbs :: BreadCrumbs -> Bool
hasNoBreadCrumbs :: BreadCrumbs -> Bool
hasNoBreadCrumbs (BreadCrumbs [BreadCrumb]
xs) = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [BreadCrumb]
xs

-- | Drop a breadcrumb on the path behind you.
breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (MatchingFields [Name]
xs) (BreadCrumbs (MatchingFields [Name]
ys : [BreadCrumb]
bcs)) =
  [BreadCrumb] -> BreadCrumbs
BreadCrumbs forall a b. (a -> b) -> a -> b
$ [Name] -> BreadCrumb
MatchingFields ([Name]
ys forall a. [a] -> [a] -> [a]
++ [Name]
xs) forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs
breadCrumb BreadCrumb
bc (BreadCrumbs [BreadCrumb]
bcs) =
  [BreadCrumb] -> BreadCrumbs
BreadCrumbs forall a b. (a -> b) -> a -> b
$ BreadCrumb
bc forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs

instance Pretty BreadCrumbs where
  pretty :: forall ann. BreadCrumbs -> Doc ann
pretty (BreadCrumbs []) = forall a. Monoid a => a
mempty
  pretty (BreadCrumbs [BreadCrumb]
bcs) = forall ann. Doc ann
line forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [BreadCrumb]
bcs)

-- | A usage that caused a type constraint.
data Usage = Usage (Maybe T.Text) SrcLoc
  deriving (Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Text -> SrcLoc -> Usage
Usage forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a => a -> SrcLoc
srclocOf

-- | 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 -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a => a -> SrcLoc
srclocOf

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

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

-- | The level at which a type variable is bound.  Higher means
-- deeper.  We can only unify a type variable at level @i@ with a type
-- @t@ if all type names that occur in @t@ are at most at level @i@.
type Level = Int

-- | A constraint on a yet-ambiguous type variable.
data Constraint
  = NoConstraint Liftedness Usage
  | ParamType Liftedness SrcLoc
  | Constraint StructRetType Usage
  | Overloaded [PrimType] Usage
  | HasFields Liftedness (M.Map Name StructType) Usage
  | Equality Usage
  | HasConstrs Liftedness (M.Map Name [StructType]) Usage
  | ParamSize SrcLoc
  | -- | 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 SrcLoc RigidSource
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show)

instance Located Constraint where
  locOf :: Constraint -> Loc
locOf (NoConstraint Liftedness
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (ParamType Liftedness
_ SrcLoc
usage) = forall a. Located a => a -> Loc
locOf SrcLoc
usage
  locOf (Constraint StructRetType
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (Overloaded [PrimType]
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (HasFields Liftedness
_ Map Name StructType
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (Equality Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (HasConstrs Liftedness
_ Map Name [StructType]
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (ParamSize SrcLoc
loc) = forall a. Located a => a -> Loc
locOf SrcLoc
loc
  locOf (Size Maybe Exp
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (UnknownSize SrcLoc
loc RigidSource
_) = forall a. Located a => a -> Loc
locOf SrcLoc
loc

-- | 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 forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
  Just (Constraint StructRetType
t Usage
_) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. [TypeParam] -> t -> Subst t
Subst [] forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) StructRetType
t
  Just (Size (Just Exp
d) Usage
_) ->
    forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Exp -> Subst t
ExpSubst forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d
  Maybe Constraint
_ -> 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))
  | RigidLoop
  | -- | Produced by a complicated slice expression.
    RigidSlice (Maybe Size) T.Text
  | -- | Produced by a complicated range expression.
    RigidRange
  | -- | Produced by a range expression with this bound.
    RigidBound T.Text
  | -- | Mismatch in branches.
    RigidCond StructType StructType
  | -- | Invented during unification.
    RigidUnify
  | RigidOutOfScope SrcLoc VName
  | -- | Blank dimension in coercion.
    RigidCoerce
  deriving (RigidSource -> RigidSource -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RigidSource -> RigidSource -> Bool
$c/= :: RigidSource -> RigidSource -> Bool
== :: RigidSource -> RigidSource -> Bool
$c== :: RigidSource -> RigidSource -> Bool
Eq, Eq 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
min :: RigidSource -> RigidSource -> RigidSource
$cmin :: RigidSource -> RigidSource -> RigidSource
max :: RigidSource -> RigidSource -> RigidSource
$cmax :: RigidSource -> RigidSource -> RigidSource
>= :: RigidSource -> RigidSource -> Bool
$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
compare :: RigidSource -> RigidSource -> Ordering
$ccompare :: RigidSource -> RigidSource -> Ordering
Ord, Int -> RigidSource -> ShowS
[RigidSource] -> ShowS
RigidSource -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RigidSource] -> ShowS
$cshowList :: [RigidSource] -> ShowS
show :: RigidSource -> String
$cshow :: RigidSource -> String
showsPrec :: Int -> RigidSource -> ShowS
$cshowsPrec :: Int -> 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c== :: Rigidity -> Rigidity -> Bool
Eq, Eq 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
min :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmax :: Rigidity -> Rigidity -> Rigidity
>= :: Rigidity -> Rigidity -> Bool
$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
compare :: Rigidity -> Rigidity -> Ordering
$ccompare :: Rigidity -> Rigidity -> Ordering
Ord, Int -> Rigidity -> ShowS
[Rigidity] -> ShowS
Rigidity -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rigidity] -> ShowS
$cshowList :: [Rigidity] -> ShowS
show :: Rigidity -> String
$cshow :: Rigidity -> String
showsPrec :: Int -> Rigidity -> ShowS
$cshowsPrec :: Int -> Rigidity -> ShowS
Show)

prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet Maybe (QualName VName)
Nothing) =
  Doc ()
"is unknown size returned by function at"
    forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet (Just QualName VName
fname)) =
  Doc ()
"is unknown size returned by"
    forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
fname)
    forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
    forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidArg Maybe (QualName VName)
fname Text
arg) =
  Doc ()
"is value of argument"
    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
arg))
    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"passed to"
    forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann
fname'
    forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
    forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
  where
    fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"function" (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) Maybe (QualName VName)
fname
prettySource SrcLoc
ctx SrcLoc
loc (RigidSlice Maybe Exp
d Text
slice) =
  Doc ()
"is size produced by slice"
    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
slice))
    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Doc ann
d_desc
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"at"
      forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    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 " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Exp
d') forall a. Semigroup a => a -> a -> a
<> Doc ann
" "
      Maybe Exp
Nothing -> forall a. Monoid a => a
mempty
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidLoop =
  Doc ()
"is unknown size of value returned at" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidRange =
  Doc ()
"is unknown length of range at" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidBound Text
bound) =
  Doc ()
"generated from expression"
    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
bound))
    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"used in range at "
    forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidOutOfScope SrcLoc
boundloc VName
v) =
  Doc ()
"is an unknown size arising from "
    forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
" going out of scope at "
    forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Originally bound at "
    forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
boundloc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidCoerce =
  Doc ()
"is an unknown size arising from empty dimension in coercion at"
    forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
_ SrcLoc
_ RigidSource
RigidUnify =
  Doc ()
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource SrcLoc
ctx SrcLoc
loc (RigidCond StructType
t1 StructType
t2) =
  Doc ()
"is unknown due to conditional expression at "
    forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"One branch returns array of type: "
    forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
      forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"The other an array of type:       "
    forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> 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
  Maybe (Int, Constraint)
c <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case Maybe (Int, Constraint)
c of
    Just (Int
_, UnknownSize SrcLoc
loc RigidSource
rsrc) ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Notes
aNote forall a b. (a -> b) -> a -> b
$
        forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
d) forall a. Doc a -> Doc a -> Doc a
<+> SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource (forall a. Located a => a -> SrcLoc
srclocOf a
ctx) SrcLoc
loc RigidSource
rsrc
    Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
dimNotes a
_ Exp
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

typeNotes :: (Located a, MonadUnify m) => a -> StructType -> m Notes
typeNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes a
ctx =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Monoid a => [a] -> a
mconcat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes a
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> Exp
sizeFromName forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. FV -> Set VName
fvVars
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall u. TypeBase Exp u -> FV
freeInType

typeVarNotes :: (MonadUnify m) => VName -> m Notes
typeVarNotes :: forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (Constraint -> Notes
note forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  where
    note :: Constraint -> Notes
note (HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
_) =
      Doc () -> Notes
aNote forall a b. (a -> b) -> a -> b
$
        forall v a. IsName v => v -> Doc a
prettyName VName
v
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"="
          forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {ann}. Pretty a => (a, b) -> Doc ann
ppConstr (forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"..."
    note (Overloaded [PrimType]
ts Usage
_) =
      Doc () -> Notes
aNote forall a b. (a -> b) -> a -> b
$ forall v a. IsName v => v -> Doc a
prettyName VName
v forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be one of" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Monoid a => [a] -> a
mconcat (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ()
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts))
    note (HasFields Liftedness
_ Map Name StructType
fs Usage
_) =
      Doc () -> Notes
aNote forall a b. (a -> b) -> a -> b
$
        forall v a. IsName v => v -> Doc a
prettyName VName
v
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"="
          forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
braces (forall a. Monoid a => [a] -> a
mconcat (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ()
", " (forall a b. (a -> b) -> [a] -> [b]
map forall {v} {b} {a}. IsName v => (v, b) -> Doc a
ppField (forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs))))
    note Constraint
_ = forall a. Monoid a => a
mempty

    ppConstr :: (a, b) -> Doc ann
ppConstr (a
c, b
_) = Doc ann
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
c forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"..." forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"|"
    ppField :: (v, b) -> Doc a
ppField (v
f, b
_) = forall v a. IsName v => v -> Doc a
prettyName v
f forall a. Semigroup a => a -> a -> a
<> Doc a
":" forall a. Doc a -> Doc a -> Doc a
<+> Doc a
"..."

-- | 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
    Constraints
x <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
    forall (m :: * -> *). MonadUnify m => Constraints -> m ()
putConstraints forall a b. (a -> b) -> a -> b
$ Constraints -> Constraints
f Constraints
x

  newTypeVar :: (Monoid als) => SrcLoc -> Name -> m (TypeBase dim als)
  newDimVar :: Usage -> Rigidity -> Name -> m VName
  newRigidDim :: (Located a) => a -> RigidSource -> Name -> m VName
  newRigidDim a
loc = forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar (forall a. Located a => a -> Usage
mkUsage' a
loc) forall b c a. (b -> c) -> (a -> b) -> a -> c
. RigidSource -> Rigidity
Rigid
  newFlexibleDim :: Usage -> Name -> m VName
  newFlexibleDim Usage
usage = 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
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) a
t

-- | Replace any top-level type variable with its substitution.
normType :: (MonadUnify m) => StructType -> m StructType
normType :: forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType t :: StructType
t@(Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) [])) = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
    Just (Constraint (RetType [] StructType
t') Usage
_) -> forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t'
    Maybe Constraint
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
normType StructType
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t

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

unsharedConstructorsMsg :: M.Map Name t -> M.Map Name t -> Doc a
unsharedConstructorsMsg :: forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name t
cs1 Map Name t
cs2 =
  Doc a
"Unshared constructors:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map ((Doc a
"#" <>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) [Name]
missing) forall a. Semigroup a => a -> a -> a
<> Doc a
"."
  where
    missing :: [Name]
missing =
      forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall k a. Map k a -> [k]
M.keys Map Name t
cs1) (forall k a. Map k a -> [k]
M.keys Map Name t
cs2)
        forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall k a. Map k a -> [k]
M.keys Map Name t
cs2) (forall k a. Map k a -> [k]
M.keys Map Name t
cs1)

-- | Is the given type variable the name of an abstract type or type
-- parameter, which we cannot substitute?
isRigid :: VName -> Constraints -> Bool
isRigid :: VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints =
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Constraint -> Bool
rigidConstraint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints

-- | 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
  (Int
lvl, Constraint
c) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Constraint -> Bool
rigidConstraint Constraint
c
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl

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

flipUnifySizes :: UnifySizes m -> UnifySizes m
flipUnifySizes :: forall (m :: * -> *). UnifySizes m -> UnifySizes m
flipUnifySizes UnifySizes m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
t1 Exp
t2 =
  UnifySizes m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
t2 Exp
t1

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
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

      StructType
t1' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t1
      StructType
t2' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t2

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

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

          link :: Bool -> VName -> Int -> StructType -> m ()
link Bool
ord' =
            forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifySizes m
linkDims Usage
usage [VName]
bound BreadCrumbs
bcs
            where
              -- We may have to flip the order of future calls to
              -- onDims inside linkVarToType.
              linkDims :: UnifySizes m
linkDims
                | Bool
ord' = forall (m :: * -> *). UnifySizes m -> UnifySizes m
flipUnifySizes UnifySizes m
onDims
                | Bool
otherwise = UnifySizes m
onDims

          unifyTypeArg :: BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Exp
d1) (TypeArgDim Exp
d2) =
            BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs' (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
bcs' TypeArg Exp
_ TypeArg Exp
_ =
            forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
              Usage
usage
              forall a. Monoid a => a
mempty
              BreadCrumbs
bcs'
              Doc ()
"Cannot unify a type argument with a dimension argument (or vice versa)."

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

      case (StructType
t1', StructType
t2') of
        (Scalar (Prim PrimType
pt1), Scalar (Prim PrimType
pt2))
          | PrimType
pt1 forall a. Eq a => a -> a -> Bool
== PrimType
pt2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        ( Scalar (Record Map Name StructType
fs),
          Scalar (Record Map Name StructType
arg_fs)
          )
            | forall k a. Map k a -> [k]
M.keys Map Name StructType
fs forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs ->
                forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
fs Map Name StructType
arg_fs
            | Bool
otherwise -> do
                let missing :: [Name]
missing =
                      forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs) (forall k a. Map k a -> [k]
M.keys Map Name StructType
fs)
                        forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall k a. Map k a -> [k]
M.keys Map Name StructType
fs) (forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs)
                forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
                  Doc ()
"Unshared fields:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
missing) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        ( Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Exp]
targs),
          Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Exp]
arg_targs)
          )
            | VName
tn forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
              forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
targs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
arg_targs -> do
                let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching type arguments.") BreadCrumbs
bcs
                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 (TypeVar NoUniqueness
_ (QualName [] VName
v1) []),
          Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v2) [])
          ) ->
            case (VName -> Maybe Int
nonrigid VName
v1, VName -> Maybe Int
nonrigid VName
v2) of
              (Maybe Int
Nothing, Maybe Int
Nothing) -> forall {a}. m a
failure
              (Just Int
lvl1, Maybe Int
Nothing) -> Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl1 StructType
t2'
              (Maybe Int
Nothing, Just Int
lvl2) -> Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl2 StructType
t1'
              (Just Int
lvl1, Just Int
lvl2)
                | Int
lvl1 forall a. Ord a => a -> a -> Bool
<= Int
lvl2 -> Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl1 StructType
t2'
                | Bool
otherwise -> Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl2 StructType
t1'
        (Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v1) []), StructType
_)
          | Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v1 ->
              Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl StructType
t2'
        (StructType
_, Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v2) []))
          | Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v2 ->
              Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl StructType
t1'
        ( Scalar (Arrow NoUniqueness
_ PName
p1 Diet
d1 StructType
a1 (RetType [VName]
b1_dims TypeBase Exp Uniqueness
b1)),
          Scalar (Arrow NoUniqueness
_ PName
p2 Diet
d2 StructType
a2 (RetType [VName]
b2_dims TypeBase Exp Uniqueness
b2))
          )
            | forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Ord a => a -> a -> Bool
(<) forall a b. (a -> b) -> a -> b
$ forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Diet
d1 Diet
d2 -> do
                forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-consuming-param" forall a b. (a -> b) -> a -> b
$
                  Doc ()
"Parameters"
                    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty Diet
d1 forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty StructType
a1)
                    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"and"
                    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty Diet
d2 forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty StructType
a2)
                    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"are incompatible regarding consuming their arguments."
            | forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Ord a => a -> a -> Bool
(<) forall a b. (a -> b) -> a -> b
$ forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord (forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness TypeBase Exp Uniqueness
b2) (forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness TypeBase Exp Uniqueness
b1) -> do
                forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-return-uniqueness" forall a b. (a -> b) -> a -> b
$
                  Doc ()
"Return types"
                    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty Diet
d1 forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty TypeBase Exp Uniqueness
b1)
                    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"and"
                    forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty Diet
d2 forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty TypeBase Exp Uniqueness
b2)
                    forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"have incompatible uniqueness."
            | 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) =
                      forall {a}. Bool -> a -> a -> (a, a)
swap
                        Bool
ord
                        (Maybe Exp -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing forall a. Monoid a => a
mempty)
                        (SrcLoc -> RigidSource -> Constraint
UnknownSize forall a. Monoid a => a
mempty RigidSource
RigidUnify)
                Int
lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
                forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. (a -> b) -> [a] -> [b]
map (,(Int
lvl, Constraint
r1)) [VName]
b1_dims) <>)
                forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. (a -> b) -> [a] -> [b]
map (,(Int
lvl, Constraint
r2)) [VName]
b2_dims) <>)

                let bound' :: [VName]
bound' = [VName]
bound forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PName -> Maybe VName
pname [PName
p1, PName
p2] forall a. Semigroup a => a -> a -> a
<> [VName]
b1_dims forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims
                Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify
                  (Bool -> Bool
not Bool
ord)
                  [VName]
bound
                  (BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching parameter types.") BreadCrumbs
bcs)
                  StructType
a1
                  StructType
a2
                Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify
                  Bool
ord
                  [VName]
bound'
                  (BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching return types.") BreadCrumbs
bcs)
                  (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Exp Uniqueness
b1')
                  (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Exp Uniqueness
b2')

                -- Delete the size variables we introduced to represent
                -- the existential sizes.
                forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ \Constraints
m -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Map k a
M.delete) Constraints
m ([VName]
b1_dims forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims)
            where
              (TypeBase Exp Uniqueness
b1', TypeBase Exp Uniqueness
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 forall a. Eq a => a -> a -> Bool
== VName
p2' = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Exp -> Subst t
ExpSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (forall v. v -> QualName v
qualName VName
p1') forall a. Monoid a => a
mempty
                          | Bool
otherwise = forall a. Maybe a
Nothing
                     in (TypeBase Exp Uniqueness
b1, forall a. Substitutable a => TypeSubs -> a -> a
applySubst forall {t}. VName -> Maybe (Subst t)
f TypeBase Exp Uniqueness
b2)
                  (PName
_, PName
_) ->
                    (TypeBase Exp Uniqueness
b1, TypeBase Exp Uniqueness
b2)

              pname :: PName -> Maybe VName
pname (Named VName
x) = forall a. a -> Maybe a
Just VName
x
              pname PName
Unnamed = forall a. Maybe a
Nothing
        (Array {}, Array {})
          | Shape (Exp
t1_d : [Exp]
_) <- forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t1',
            Shape (Exp
t2_d : [Exp]
_) <- forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t2',
            Just StructType
t1'' <- forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
peelArray Int
1 StructType
t1',
            Just StructType
t2'' <- forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
peelArray Int
1 StructType
t2' -> do
              BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs (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 StructType
t1'' StructType
t2''
        ( Scalar (Sum Map Name [StructType]
cs),
          Scalar (Sum Map Name [StructType]
arg_cs)
          )
            | forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs ->
                forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs Map Name [StructType]
arg_cs
            | Bool
otherwise ->
                forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$ forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name [StructType]
arg_cs Map Name [StructType]
cs
        (StructType, StructType)
_ -> forall {a}. m a
failure

anyBound :: [VName] -> ExpBase Info VName -> Bool
anyBound :: [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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 =
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ 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 (forall vn. QualName vn -> vn
qualLeaf QualName VName
v1),
    Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e2) Bool -> Bool -> Bool
|| (forall vn. QualName vn -> vn
qualLeaf QualName VName
v1 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
      forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (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 (forall vn. QualName vn -> vn
qualLeaf QualName VName
v2),
    Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e1) Bool -> Bool -> Bool
|| (forall vn. QualName vn -> vn
qualLeaf QualName VName
v2 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
      forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (forall vn. QualName vn -> vn
qualLeaf QualName VName
v2) Int
lvl2 Exp
e1
unifySizes Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Exp
e1 Exp
e2 = do
  Notes
notes <- forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e2
  forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
    Doc ()
"Sizes"
      forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Exp
e1)
      forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"and"
      forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Exp
e2)
      forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"do not match."

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

occursCheck ::
  (MonadUnify m) =>
  Usage ->
  BreadCrumbs ->
  VName ->
  StructType ->
  m ()
occursCheck :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp =
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
vn forall a. Ord a => a -> Set a -> Bool
`S.member` forall dim as. TypeBase dim as -> Set VName
typeVars StructType
tp) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
      Doc ()
"Occurs check: cannot instantiate"
        forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn
        forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with"
        forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp
        forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

scopeCheck ::
  (MonadUnify m) =>
  Usage ->
  BreadCrumbs ->
  VName ->
  Level ->
  StructType ->
  m ()
scopeCheck :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
vn Int
max_lvl StructType
tp = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  forall {m :: * -> *} {u}.
MonadUnify m =>
Constraints -> TypeBase Exp u -> m ()
checkType Constraints
constraints StructType
tp
  where
    checkType :: Constraints -> TypeBase Exp u -> m ()
checkType Constraints
constraints TypeBase Exp u
t =
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
check Constraints
constraints) forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> Set VName
typeVars TypeBase Exp u
t forall a. Semigroup a => a -> a -> a
<> FV -> Set VName
fvVars (forall u. TypeBase Exp u -> FV
freeInType TypeBase Exp u
t)

    check :: Constraints -> VName -> m ()
check Constraints
constraints VName
v
      | Just (Int
lvl, Constraint
c) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints,
        Int
lvl forall a. Ord a => a -> a -> Bool
> Int
max_lvl =
          if Constraint -> Bool
rigidConstraint Constraint
c
            then forall {m :: * -> *} {v} {b}. (MonadUnify m, IsName v) => v -> m b
scopeViolation VName
v
            else forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
max_lvl, Constraint
c)
      | Bool
otherwise =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    scopeViolation :: v -> m b
scopeViolation v
v = do
      Notes
notes <- forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes Usage
usage StructType
tp
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot unify type"
          forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
          forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"with"
          forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"(scope violation)."
          forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"This is because"
          forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
v)
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is rigidly bound in a deeper scope."

linkVarToType ::
  (MonadUnify m) =>
  UnifySizes m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  VName ->
  Level ->
  StructType ->
  m ()
linkVarToType :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs VName
vn Int
lvl StructType
tp_unnorm = do
  -- We have to expand anyway for the occurs check, so we might as
  -- well link the fully expanded type.
  StructType
tp <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
tp_unnorm
  forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp
  forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
vn Int
lvl StructType
tp

  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  let link :: m ()
link = do
        let (Set VName
witnessed, Set VName
not_witnessed) = StructType -> (Set VName, Set VName)
determineSizeWitnesses StructType
tp
            used :: VName -> Bool
used VName
v = VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
witnessed Bool -> Bool -> Bool
|| VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
not_witnessed
            ext :: [VName]
ext = forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
used [VName]
bound
        case forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set VName
witnessed) [VName]
ext of
          [] ->
            forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
              forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp) Usage
usage)
          [VName]
problems ->
            forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-param-existential" forall a b. (a -> b) -> a -> b
$
              Doc ()
"Parameter(s) "
                forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v a. IsName v => v -> Doc a
prettyName) [VName]
problems)
                forall a. Semigroup a => a -> a -> a
<> Doc ()
" used as size(s) would go out of scope."

  let unliftedBcs :: a -> BreadCrumbs
unliftedBcs a
unlifted_usage =
        BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
          ( Doc () -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$
              Doc ()
"When verifying that"
                forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
                forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
"is not instantiated with a function type, due to"
                forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
unlifted_usage
          )
          BreadCrumbs
bcs

  case forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
    Just (NoConstraint Liftedness
Unlifted Usage
unlift_usage) -> do
      m ()
link

      forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
unlift_usage) StructType
tp
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) (FV -> Set VName
fvVars (forall u. TypeBase Exp u -> FV
freeInType StructType
tp))) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
          Doc ()
"Type variable"
            forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn
            forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"cannot be instantiated with type containing anonymous sizes:"
            forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
            forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"This is usually because the size of an array returned by a higher-order function argument cannot be determined statically.  This can also be due to the return size being a value parameter.  Add type annotation to clarify."
    Just (Equality Usage
_) -> do
      m ()
link
      forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> TypeBase dim u -> m ()
equalityType Usage
usage StructType
tp
    Just (Overloaded [PrimType]
ts Usage
old_usage)
      | StructType
tp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim u. PrimType -> ScalarTypeBase dim u
Prim) [PrimType]
ts -> do
          m ()
link
          case StructType
tp of
            Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) [])
              | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints ->
                  forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
            StructType
_ ->
              forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
                Doc ()
"Cannot instantiate"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
                  forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
                  forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be one of"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
                  forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
old_usage
                  forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    Just (HasFields Liftedness
l Map Name StructType
required_fields Usage
old_usage) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Liftedness
l forall a. Eq a => a -> a -> Bool
== Liftedness
Unlifted) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
old_usage) StructType
tp
      case StructType
tp of
        Scalar (Record Map Name StructType
tp_fields)
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map Name StructType
tp_fields) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map Name StructType
required_fields -> do
              Map Name StructType
required_fields' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully Map Name StructType
required_fields
              let tp' :: StructType
tp' = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record forall a b. (a -> b) -> a -> b
$ Map Name StructType
required_fields forall a. Semigroup a => a -> a -> a
<> Map Name StructType
tp_fields -- Crucially left-biased.
                  ext :: [VName]
ext = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (forall u. TypeBase Exp u -> FV
freeInType StructType
tp')) [VName]
bound
              forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
                forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp') Usage
usage)
              forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
required_fields' Map Name StructType
tp_fields
        Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) []) -> do
          case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
            Just (Int
_, HasFields Liftedness
_ Map Name StructType
tp_fields Usage
_) ->
              forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
required_fields Map Name StructType
tp_fields
            Just (Int
_, NoConstraint {}) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just (Int
_, Equality {}) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Maybe (Int, Constraint)
_ -> do
              Notes
notes <- forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v
              forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noRecordType Notes
notes
          m ()
link
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
            forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith
              forall {a}.
(Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineFields
              VName
v
              (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
l Map Name StructType
required_fields Usage
old_usage)
          where
            combineFields :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineFields (Int
_, HasFields Liftedness
l1 Map Name StructType
fs1 Usage
usage1) (a
_, HasFields Liftedness
l2 Map Name StructType
fs2 Usage
_) =
              (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields (Liftedness
l1 forall a. Ord a => a -> a -> a
`min` Liftedness
l2) (forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Name StructType
fs1 Map Name StructType
fs2) Usage
usage1)
            combineFields (Int, Constraint)
hasfs (a, Constraint)
_ = (Int, Constraint)
hasfs
        StructType
_ ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot instantiate"
              forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
              forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
              forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
              forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be a record with fields"
              forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty (forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record Map Name StructType
required_fields))
              forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
old_usage
              forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    -- See Note [Linking variables to sum types]
    Just (HasConstrs Liftedness
l Map Name [StructType]
required_cs Usage
old_usage) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Liftedness
l forall a. Eq a => a -> a -> Bool
== Liftedness
Unlifted) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
old_usage) StructType
tp
      case StructType
tp of
        Scalar (Sum Map Name [StructType]
ts)
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map Name [StructType]
ts) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Map Name [StructType]
required_cs -> do
              let tp' :: StructType
tp' = forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum forall a b. (a -> b) -> a -> b
$ Map Name [StructType]
required_cs forall a. Semigroup a => a -> a -> a
<> Map Name [StructType]
ts -- Crucially left-biased.
                  ext :: [VName]
ext = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (forall u. TypeBase Exp u -> FV
freeInType StructType
tp')) [VName]
bound
              forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
                forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp') Usage
usage)
              forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
ts
          | Bool
otherwise ->
              forall {m :: * -> *} {t} {a}.
MonadUnify m =>
Map Name t -> Map Name t -> Notes -> m a
unsharedConstructors Map Name [StructType]
required_cs Map Name [StructType]
ts forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn
        Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) []) -> do
          case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
            Just (Int
_, HasConstrs Liftedness
_ Map Name [StructType]
v_cs Usage
_) ->
              forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
v_cs
            Just (Int
_, NoConstraint {}) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just (Int
_, Equality {}) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Maybe (Int, Constraint)
_ -> do
              Notes
notes <- forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v
              forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noSumType Notes
notes
          m ()
link
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
            forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith
              forall {a}.
(Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs
              VName
v
              (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l Map Name [StructType]
required_cs Usage
old_usage)
          where
            combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs (Int
_, HasConstrs Liftedness
l1 Map Name [StructType]
cs1 Usage
usage1) (a
_, HasConstrs Liftedness
l2 Map Name [StructType]
cs2 Usage
_) =
              (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs (Liftedness
l1 forall a. Ord a => a -> a -> a
`min` Liftedness
l2) (forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Name [StructType]
cs1 Map Name [StructType]
cs2) Usage
usage1)
            combineConstrs (Int, Constraint)
hasCs (a, Constraint)
_ = (Int, Constraint)
hasCs
        StructType
_ -> forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noSumType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn
    Maybe Constraint
_ -> m ()
link
  where
    unsharedConstructors :: Map Name t -> Map Name t -> Notes -> m a
unsharedConstructors Map Name t
cs1 Map Name t
cs2 Notes
notes =
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
        Usage
usage
        Notes
notes
        BreadCrumbs
bcs
        (forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name t
cs1 Map Name t
cs2)
    noSumType :: Notes -> m a
noSumType Notes
notes =
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
        Usage
usage
        Notes
notes
        BreadCrumbs
bcs
        Doc ()
"Cannot unify a sum type with a non-sum type."
    noRecordType :: Notes -> m a
noRecordType Notes
notes =
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
        Usage
usage
        Notes
notes
        BreadCrumbs
bcs
        Doc ()
"Cannot unify a record type with a non-record type."

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
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
checkVar Constraints
constraints) forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars forall a b. (a -> b) -> a -> b
$ Exp -> FV
freeInExp Exp
e

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

-- | Assert that this type must be one of the given primitive types.
mustBeOneOf :: (MonadUnify m) => [PrimType] -> Usage -> StructType -> m ()
mustBeOneOf :: forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType
req_t] Usage
usage StructType
t = forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
req_t)) StructType
t
mustBeOneOf [PrimType]
ts Usage
usage StructType
t = do
  StructType
t' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  let isRigid' :: VName -> Bool
isRigid' VName
v = VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints

  case StructType
t' of
    Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) [])
      | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ VName -> Bool
isRigid' VName
v -> forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
    Scalar (Prim PrimType
pt) | PrimType
pt forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ts -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    StructType
_ -> forall {a}. m a
failure
  where
    failure :: m a
failure =
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot unify type"
          forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t)
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with any of "
          forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
          forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

linkVarToTypes :: (MonadUnify m) => Usage -> VName -> [PrimType] -> m ()
linkVarToTypes :: forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
vn [PrimType]
ts = do
  Maybe (Int, Constraint)
vn_constraint <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case Maybe (Int, Constraint)
vn_constraint of
    Just (Int
lvl, Overloaded [PrimType]
vn_ts Usage
vn_usage) ->
      case [PrimType]
ts forall a. Eq a => [a] -> [a] -> [a]
`intersect` [PrimType]
vn_ts of
        [] ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Type constrained to one of"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"but also one of"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
vn_ts)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"due to"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage
              forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        [PrimType]
ts' -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts' Usage
usage)
    Just (Int
_, HasConstrs Liftedness
_ Map Name [StructType]
_ Usage
vn_usage) ->
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constrained to one of"
          forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
          forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be sum type due to"
            forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage
          forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    Just (Int
_, HasFields Liftedness
_ Map Name StructType
_ Usage
vn_usage) ->
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constrained to one of"
          forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
          forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be record due to"
            forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage
          forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    Just (Int
lvl, Constraint
_) -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts Usage
usage)
    Maybe (Int, Constraint)
Nothing ->
      forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot constrain type to one of" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)

-- | Assert that this type must support equality.
equalityType ::
  (MonadUnify m, Pretty (Shape dim), Pretty u) =>
  Usage ->
  TypeBase dim u ->
  m ()
equalityType :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> TypeBase dim u -> m ()
equalityType Usage
usage TypeBase dim u
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim u
t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
      Doc ()
"Type " forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim u
t) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality (may contain function)."
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeEquality forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> Set VName
typeVars TypeBase dim u
t
  where
    mustBeEquality :: VName -> m ()
mustBeEquality VName
vn = do
      Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
      case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
        Just (Int
_, Constraint (RetType [] (Scalar (TypeVar NoUniqueness
_ (QualName [] VName
vn') []))) Usage
_) ->
          VName -> m ()
mustBeEquality VName
vn'
        Just (Int
_, Constraint (RetType [VName]
_ StructType
vn_t) Usage
cusage)
          | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> Bool
orderZero StructType
vn_t ->
              forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
                Doc ()
"Type"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim u
t)
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."
                  forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Constrained to be higher-order due to"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
cusage
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
          | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Usage -> Constraint
Equality Usage
usage)
        Just (Int
_, Overloaded [PrimType]
_ Usage
_) ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- All primtypes support equality.
        Just (Int
_, Equality {}) ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just (Int
_, HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
_) ->
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> TypeBase dim u -> m ()
equalityType Usage
usage) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems Map Name [StructType]
cs
        Maybe (Int, Constraint)
_ ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Type" forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."

zeroOrderTypeWith ::
  (MonadUnify m) =>
  Usage ->
  BreadCrumbs ->
  StructType ->
  m ()
zeroOrderTypeWith :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> StructType -> m ()
zeroOrderTypeWith Usage
usage BreadCrumbs
bcs StructType
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero StructType
t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
      Doc ()
"Type" forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t) forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> Set VName
typeVars forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
  where
    mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
      Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
      case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
        Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted Usage
usage)
        Just (Int
lvl, HasFields Liftedness
_ Map Name StructType
fs Usage
_) ->
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
Unlifted Map Name StructType
fs Usage
usage)
        Just (Int
lvl, HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
_) ->
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
Unlifted Map Name [StructType]
cs Usage
usage)
        Just (Int
_, ParamType Liftedness
Lifted SrcLoc
ploc) ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Type parameter"
              forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> String
locStr SrcLoc
ploc)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"may be a function."
        Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Assert that this type must be zero-order.
zeroOrderType ::
  (MonadUnify m) => Usage -> T.Text -> StructType -> m ()
zeroOrderType :: forall (m :: * -> *).
MonadUnify m =>
Usage -> Text -> StructType -> m ()
zeroOrderType Usage
usage Text
desc =
  forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> StructType -> m ()
zeroOrderTypeWith Usage
usage forall a b. (a -> b) -> a -> b
$ BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb BreadCrumb
bc BreadCrumbs
noBreadCrumbs
  where
    bc :: BreadCrumb
bc = Doc () -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$ Doc ()
"When checking" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
desc

arrayElemTypeWith ::
  (MonadUnify m, Pretty (Shape dim), Pretty u) =>
  Usage ->
  BreadCrumbs ->
  TypeBase dim u ->
  m ()
arrayElemTypeWith :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim u
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim u
t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
      Doc ()
"Type" forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim u
t) forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ TypeBase dim u
t
  where
    mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
      Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
      case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
        Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted Usage
usage)
        Just (Int
_, ParamType Liftedness
l SrcLoc
ploc)
          | Liftedness
l forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Liftedness
Lifted, Liftedness
SizeLifted] ->
              forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
                Doc ()
"Type parameter"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"bound at"
                  forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> String
locStr SrcLoc
ploc)
                  forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is lifted and cannot be an array element."
        Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Assert that this type must be valid as an array element.
arrayElemType ::
  (MonadUnify m, Pretty (Shape dim), Pretty u) =>
  Usage ->
  T.Text ->
  TypeBase dim u ->
  m ()
arrayElemType :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> Text -> TypeBase dim u -> m ()
arrayElemType Usage
usage Text
desc =
  forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage forall a b. (a -> b) -> a -> b
$ BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb BreadCrumb
bc BreadCrumbs
noBreadCrumbs
  where
    bc :: BreadCrumb
bc = Doc () -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$ Doc ()
"When checking" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
desc

unifySharedFields ::
  (MonadUnify m) =>
  UnifySizes m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  M.Map Name StructType ->
  M.Map Name StructType ->
  m ()
unifySharedFields :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
fs1 Map Name StructType
fs2 =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name StructType
fs1 Map Name StructType
fs2) forall a b. (a -> b) -> a -> b
$ \(Name
f, (StructType
t1, StructType
t2)) ->
    forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound (BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
f]) BreadCrumbs
bcs) StructType
t1 StructType
t2

unifySharedConstructors ::
  (MonadUnify m) =>
  UnifySizes m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  M.Map Name [StructType] ->
  M.Map Name [StructType] ->
  m ()
unifySharedConstructors :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs1 Map Name [StructType]
cs2 =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [StructType]
cs1 Map Name [StructType]
cs2) forall a b. (a -> b) -> a -> b
$ \(Name
c, ([StructType]
f1, [StructType]
f2)) ->
    Name -> [StructType] -> [StructType] -> m ()
unifyConstructor Name
c [StructType]
f1 [StructType]
f2
  where
    unifyConstructor :: Name -> [StructType] -> [StructType] -> m ()
unifyConstructor Name
c [StructType]
f1 [StructType]
f2
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f2 = do
          let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Name -> BreadCrumb
MatchingConstructor Name
c) BreadCrumbs
bcs
          forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') [StructType]
f1 [StructType]
f2
      | Bool
otherwise =
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Cannot unify constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName Name
c) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

-- | In @mustHaveConstr usage c t fs@, the type @t@ must have a
-- constructor named @c@ that takes arguments of types @ts@.
mustHaveConstr ::
  (MonadUnify m) =>
  Usage ->
  Name ->
  StructType ->
  [StructType] ->
  m ()
mustHaveConstr :: forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
c StructType
t [StructType]
fs = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  case StructType
t of
    Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [])
      | Just (Int
lvl, NoConstraint Liftedness
l Usage
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
noBreadCrumbs VName
tn Int
lvl) [StructType]
fs
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l (forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs) Usage
usage)
      | Just (Int
lvl, HasConstrs Liftedness
l Map Name [StructType]
cs Usage
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints ->
          case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
c Map Name [StructType]
cs of
            Maybe [StructType]
Nothing ->
              forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
                forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
c [StructType]
fs Map Name [StructType]
cs) Usage
usage)
            Just [StructType]
fs'
              | forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs' -> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage) [StructType]
fs [StructType]
fs'
              | Bool
otherwise ->
                  forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
                    Doc ()
"Different arity for constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    Scalar (Sum Map Name [StructType]
cs) ->
      case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
c Map Name [StructType]
cs of
        Maybe [StructType]
Nothing ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Constuctor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"not present in type."
        Just [StructType]
fs'
          | forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs' -> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage) [StructType]
fs [StructType]
fs'
          | Bool
otherwise ->
              forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
                Doc ()
"Different arity for constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
    StructType
_ ->
      forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs

mustHaveFieldWith ::
  (MonadUnify m) =>
  UnifySizes m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  Name ->
  StructType ->
  m StructType
mustHaveFieldWith :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Name
-> StructType
-> m StructType
mustHaveFieldWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l StructType
t = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  StructType
l_type <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Name
"t"
  case StructType
t of
    Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [])
      | Just (Int
lvl, NoConstraint {}) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
          forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
tn Int
lvl StructType
l_type
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
Lifted (forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type) Usage
usage)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type
      | Just (Int
lvl, HasFields Liftedness
lifted Map Name StructType
fields Usage
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
          case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name StructType
fields of
            Just StructType
t' -> forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs StructType
l_type StructType
t'
            Maybe StructType
Nothing ->
              forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
                forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
                  VName
tn
                  (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
lifted (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
l StructType
l_type Map Name StructType
fields) Usage
usage)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type
    Scalar (Record Map Name StructType
fields)
      | Just StructType
t' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name StructType
fields -> do
          forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
l_type StructType
t'
          forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t'
      | Bool
otherwise ->
          forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
            Doc ()
"Attempt to access field"
              forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
l)
              forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
" of value of type"
              forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. TypeBase dim as -> TypeBase () ()
toStructural StructType
t)
              forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    StructType
_ -> do
      forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type
      forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type

-- | Assert that some type must have a field with this name and type.
mustHaveField ::
  (MonadUnify m) =>
  Usage ->
  Name ->
  StructType ->
  m StructType
mustHaveField :: forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField Usage
usage = forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Name
-> StructType
-> m StructType
mustHaveFieldWith (forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage) Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs

newDimOnMismatch ::
  (MonadUnify m) =>
  SrcLoc ->
  StructType ->
  StructType ->
  m (StructType, [VName])
newDimOnMismatch :: forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> StructType -> StructType -> m (StructType, [VName])
newDimOnMismatch SrcLoc
loc StructType
t1 StructType
t2 = do
  (StructType
t, Map (Exp, Exp) VName
seen) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall as (m :: * -> *) d1 d2.
(Monoid as, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
matchDims 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) forall a. Monoid a => a
mempty
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType
t, forall k a. Map k a -> [a]
M.elems Map (Exp, Exp) VName
seen)
  where
    r :: RigidSource
r = StructType -> StructType -> RigidSource
RigidCond StructType
t1 StructType
t2
    onDims :: p -> Exp -> Exp -> t m Exp
onDims p
_ Exp
d1 Exp
d2
      | Exp
d1 forall a. Eq a => a -> a -> Bool
== Exp
d2 = 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 VName
maybe_d <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Exp
d1, Exp
d2)
          case Maybe VName
maybe_d of
            Just VName
d -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (forall v. v -> QualName v
qualName VName
d) SrcLoc
loc
            Maybe VName
Nothing -> do
              VName
d <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim SrcLoc
loc RigidSource
r Name
"differ"
              forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Exp
d1, Exp
d2) VName
d
              forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (forall v. v -> QualName v
qualName VName
d) SrcLoc
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
  -- We are ignoring the dimensions here, because any mismatches
  -- should be turned into fresh size variables.
  let allOK :: p -> p -> p -> p -> p -> f ()
allOK p
_ p
_ p
_ p
_ p
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith forall {f :: * -> *} {p} {p} {p} {p} {p}.
Applicative f =>
p -> p -> p -> p -> p -> f ()
allOK Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs StructType
t1 StructType
t2
  StructType
t1' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t1
  StructType
t2' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2
  forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> StructType -> StructType -> m (StructType, [VName])
newDimOnMismatch (forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) StructType
t1' StructType
t2'

-- Simple MonadUnify implementation.

type UnifyMState = (Constraints, Int)

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

newVar :: Name -> UnifyM VName
newVar :: Name -> UnifyM VName
newVar Name
name = do
  (Constraints
x, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Constraints
x, Int
i forall a. Num a => a -> a -> a
+ Int
1)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> Int -> VName
VName (Name -> Int -> Name
mkTypeVarName Name
name Int
i) Int
i

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

  newTypeVar :: forall als dim.
Monoid als =>
SrcLoc -> Name -> UnifyM (TypeBase dim als)
newTypeVar SrcLoc
loc Name
name = do
    VName
v <- Name -> UnifyM VName
newVar Name
name
    forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Lifted forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar forall a. Monoid a => a
mempty (forall v. v -> QualName v
qualName VName
v) []

  newDimVar :: Usage -> Rigidity -> Name -> UnifyM VName
newDimVar Usage
usage Rigidity
rigidity Name
name = do
    VName
dim <- Name -> UnifyM VName
newVar Name
name
    case Rigidity
rigidity of
      Rigid RigidSource
src ->
        forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
          forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, SrcLoc -> RigidSource -> Constraint
UnknownSize (forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) RigidSource
src)
      Rigidity
Nonrigid ->
        forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
          forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, Maybe Exp -> Usage -> Constraint
Size forall a. Maybe a
Nothing Usage
usage)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim

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

  unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc ()
doc =
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ Doc ()
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> 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 =
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
    where
      doc :: Doc a
doc =
        Doc a
"Types"
          forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
          forall a. Doc a -> Doc a -> Doc a
</> Doc a
"and"
          forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
          forall a. Doc a -> Doc a -> Doc a
</> 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 (Constraints, Int) (Except TypeError) a
m) =
  forall e a. Except e a -> Either e a
runExcept forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (Constraints, Int) (Except TypeError) a
m (Constraints
constraints, Int
0)
  where
    constraints :: Constraints
constraints =
      forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
nonrigid [TypeParam]
nonrigid_tparams forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
rigid [TypeParam]
rigid_tparams
    nonrigid :: TypeParamBase a -> (a, (a, Constraint))
nonrigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, Maybe Exp -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc))
    nonrigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
l forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc))
    rigid :: TypeParamBase a -> (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, SrcLoc -> Constraint
ParamSize SrcLoc
loc))
    rigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc))

-- | Perform a unification of two types outside a monadic context.
-- The first list of type parameters are rigid but may have liftedness
-- constraints; the second list of type parameters are allowed to be
-- instantiated. All other types are considered rigid with no
-- constraints.
doUnification ::
  Loc ->
  [TypeParam] ->
  [TypeParam] ->
  StructType ->
  StructType ->
  Either TypeError StructType
doUnification :: Loc
-> [TypeParam]
-> [TypeParam]
-> StructType
-> StructType
-> Either TypeError StructType
doUnification Loc
loc [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams StructType
t1 StructType
t2 =
  forall a.
[TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing (forall a. Located a => a -> SrcLoc
srclocOf Loc
loc)) StructType
t1 StructType
t2
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2

-- Note [Linking variables to sum types]
--
-- Consider the case when unifying a result type
--
--   i32 -> ?[n].(#foo [n]bool)
--
-- with
--
--   i32 -> ?[k].a
--
-- where 'a' has a HasConstrs constraint saying that it must have at
-- least a constructor of type '#foo [0]bool'.
--
-- This unification should succeed, but we must not merely link 'a' to
-- '#foo [n]bool', as 'n' is not free.  Instead we should instantiate
-- 'a' to be a concrete sum type (because now we know exactly which
-- constructor labels it must have), and unify each of its constructor
-- payloads with the corresponding expected payload.