-- | 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,
    normPatType,
    normTypeFully,
    instantiateEmptyArrayDims,
    unify,
    expect,
    unifyMostCommon,
    doUnification,
  )
where

import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Data.Bifunctor
import Data.Char (isAscii)
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 :: SrcLoc -> T.Text -> Usage
mkUsage :: SrcLoc -> 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)

-- | Construct a 'Usage' that has just a location, but no particular
-- description.
mkUsage' :: SrcLoc -> Usage
mkUsage' :: SrcLoc -> Usage
mkUsage' = Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing

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 Size) 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.
    UnknowableSize 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 Size
_ Usage
usage) = forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (UnknowableSize 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 Overloaded {} -> forall a. a -> Maybe a
Just forall t. Subst t
PrimSubst
  Just (Size (Just Size
d) Usage
_) ->
    forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
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 Size
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 Size
d of
      Just Size
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 Size
d') forall a. Semigroup a => a -> a -> a
<> Doc ann
" "
      Maybe Size
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 -> Size -> m Notes
dimNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes a
ctx (NamedSize QualName VName
d) = 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
_, UnknowableSize 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
_ Size
_ = 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 -> Size -> m Notes
dimNotes a
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize 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
. forall as. TypeBase Size as -> Set VName
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 :: SrcLoc -> Rigidity -> Name -> m VName

  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 ()
_ Uniqueness
_ (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

-- | Replace any top-level type variable with its substitution.
normPatType :: MonadUnify m => PatType -> m PatType
normPatType :: forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType t :: PatType
t@(Scalar (TypeVar Aliasing
als Uniqueness
u (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 => PatType -> m PatType
normPatType forall a b. (a -> b) -> a -> b
$ StructType
t' forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
u forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` Aliasing
als
    Maybe Constraint
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t
normPatType PatType
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t

rigidConstraint :: Constraint -> Bool
rigidConstraint :: Constraint -> Bool
rigidConstraint ParamType {} = Bool
True
rigidConstraint ParamSize {} = Bool
True
rigidConstraint UnknowableSize {} = 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)

-- | Instantiate existential context in return type.
instantiateEmptyArrayDims ::
  MonadUnify m =>
  SrcLoc ->
  Rigidity ->
  RetTypeBase Size als ->
  m (TypeBase Size als, [VName])
instantiateEmptyArrayDims :: forall (m :: * -> *) als.
MonadUnify m =>
SrcLoc
-> Rigidity
-> RetTypeBase Size als
-> m (TypeBase Size als, [VName])
instantiateEmptyArrayDims SrcLoc
tloc Rigidity
r (RetType [VName]
dims TypeBase Size als
t) = do
  [VName]
dims' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> m VName
new [VName]
dims
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(VName, VName)] -> Size -> Size
onDim forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims [VName]
dims') TypeBase Size als
t, [VName]
dims')
  where
    new :: VName -> m VName
new = forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
tloc Rigidity
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
nameFromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> String
baseString
    onDim :: [(VName, VName)] -> Size -> Size
onDim [(VName, VName)]
dims' (NamedSize QualName VName
d) =
      QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe QualName VName
d forall v. v -> QualName v
qualName (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) [(VName, VName)]
dims')
    onDim [(VName, VName)]
_ Size
d = Size
d

-- | 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 UnifyDims m =
  BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Size -> Size -> m ()

flipUnifyDims :: UnifyDims m -> UnifyDims m
flipUnifyDims :: forall (m :: * -> *). UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t1 Size
t2 =
  UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t2 Size
t1

unifyWith ::
  MonadUnify m =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  StructType ->
  StructType ->
  m ()
unifyWith :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims m
linkDims Usage
usage [VName]
bound BreadCrumbs
bcs
            where
              -- We may have to flip the order of future calls to
              -- onDims inside linkVarToType.
              linkDims :: UnifyDims m
linkDims
                | Bool
ord' = forall (m :: * -> *). UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims
                | Bool
otherwise = UnifyDims m
onDims

          unifyTypeArg :: BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Size
d1 SrcLoc
_) (TypeArgDim Size
d2 SrcLoc
_) =
            BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Size
d1 Size
d2)
          unifyTypeArg BreadCrumbs
bcs' (TypeArgType StructType
t SrcLoc
_) (TypeArgType StructType
arg_t SrcLoc
_) =
            Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
t StructType
arg_t
          unifyTypeArg BreadCrumbs
bcs' TypeArg Size
_ TypeArg Size
_ =
            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 -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (Size
d1, Size
d2) =
            UnifyDims 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) Size
d1)
              (forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d2)

      case (StructType
t1', StructType
t2') of
        ( 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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifyDims 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 ()
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Size]
targs),
          Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Size]
arg_targs)
          )
            | VName
tn forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
              forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
targs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
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 Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Size]
targs [TypeArg Size]
arg_targs
        ( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v1) []),
          Scalar (TypeVar ()
_ Uniqueness
_ (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 ()
_ Uniqueness
_ (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 ()
_ Uniqueness
_ (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 ()
_ PName
p1 Diet
d1 StructType
a1 (RetType [VName]
b1_dims StructType
b1)),
          Scalar (Arrow ()
_ PName
p2 Diet
d2 StructType
a2 (RetType [VName]
b2_dims StructType
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."
            | 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 Size -> 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
UnknowableSize 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)]
zip [VName]
b1_dims forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (Int
lvl, Constraint
r1)) <>)
                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)]
zip [VName]
b2_dims forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (Int
lvl, Constraint
r2)) <>)

                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)
                  StructType
b1'
                  StructType
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
              (StructType
b1', StructType
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. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
p1'
                          | Bool
otherwise = forall a. Maybe a
Nothing
                     in (StructType
b1, forall a. Substitutable a => TypeSubs -> a -> a
applySubst forall {t}. VName -> Maybe (Subst t)
f StructType
b2)
                  (PName
_, PName
_) ->
                    (StructType
b1, StructType
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 (Size
t1_d : [Size]
_) <- forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t1',
            Shape (Size
t2_d : [Size]
_) <- forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t2',
            Just StructType
t1'' <- forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t1',
            Just StructType
t2'' <- forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t2' -> do
              BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs (forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Size
t1_d Size
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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims 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)
_
          | StructType
t1' forall a. Eq a => a -> a -> Bool
== StructType
t2' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          | Bool
otherwise -> forall {a}. m a
failure

unifyDims :: MonadUnify m => Usage -> UnifyDims m
unifyDims :: forall (m :: * -> *). MonadUnify m => Usage -> UnifyDims m
unifyDims Usage
_ BreadCrumbs
_ [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2
  | Size
d1 forall a. Eq a => a -> a -> Bool
== Size
d2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
  | Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1 =
      forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
  | Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2 =
      forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2 = 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 -> Size -> m Notes
dimNotes Usage
usage Size
d1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
  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 ()
"Dimensions"
      forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d1)
      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 Size
d2)
      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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith (forall (m :: * -> *). MonadUnify m => Usage -> UnifyDims m
unifyDims Usage
usage) Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs

-- | @expect super sub@ checks that @sub@ is a subtype of @super@.
expect :: MonadUnify m => Usage -> StructType -> StructType -> m ()
expect :: forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
expect Usage
usage = forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith forall {f :: * -> *} {t :: * -> *}.
(Foldable t, MonadUnify f) =>
BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
  where
    onDims :: BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims BreadCrumbs
_ t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2
      | Size
d1 forall a. Eq a => a -> a -> Bool
== Size
d2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- We identify existentially bound names by them being nonrigid
    -- and yet bound.  It's OK to unify with those.
    onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
      | Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1,
        Bool -> Bool
not (forall {t :: * -> *}. Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d2) Bool -> Bool -> Bool
|| (VName
d1 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
          forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
    onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
      | Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2,
        Bool -> Bool
not (forall {t :: * -> *}. Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d1) Bool -> Bool -> Bool
|| (VName
d2 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
          forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
    onDims BreadCrumbs
bcs t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2 = 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 -> Size -> m Notes
dimNotes Usage
usage Size
d1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
      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 ()
"Dimensions"
          forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d1)
          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 Size
d2)
          forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"do not match."

    boundParam :: t VName -> Size -> Bool
boundParam t VName
bound (NamedSize (QualName [VName]
_ VName
d)) = VName
d forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound
    boundParam t VName
_ Size
_ = Bool
False

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 as dim. Monoid 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 :: * -> *} {as}.
(MonadUnify m, Monoid as) =>
Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints StructType
tp
  where
    checkType :: Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints TypeBase Size as
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 as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size as
t forall a. Semigroup a => a -> a -> a
<> forall as. TypeBase Size as -> Set VName
freeInType TypeBase Size as
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 =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  VName ->
  Level ->
  StructType ->
  m ()
linkVarToType :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims 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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> 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) (forall as. TypeBase Size as -> Set VName
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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> 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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim) [PrimType]
ts -> do
          m ()
link
          case StructType
tp of
            Scalar (TypeVar ()
_ Uniqueness
_ (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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> 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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
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` forall as. TypeBase Size as -> Set VName
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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
required_fields' Map Name StructType
tp_fields
        Scalar (TypeVar ()
_ Uniqueness
_ (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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifyDims 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 as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> 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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
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` forall as. TypeBase Size as -> Set VName
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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims 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 ()
_ Uniqueness
_ (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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims 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 ->
  Size ->
  m ()
linkVarToDim :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
vn Int
lvl Size
dim = do
  Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints

  case Size
dim of
    NamedSize QualName VName
dim'
      | Just (Int
dim_lvl, Constraint
c) <- forall vn. QualName vn -> vn
qualLeaf QualName 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 -> Size -> m Notes
dimNotes Usage
usage Size
dim
              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 QualName VName
dim')
                  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 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 (forall vn. QualName vn -> vn
qualLeaf QualName VName
dim') (Int
lvl, Constraint
c)
    Size
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  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 Size -> Usage -> Constraint
Size (forall a. a -> Maybe a
Just Size
dim) Usage
usage)

-- | 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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as. PrimType -> ScalarTypeBase dim as
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 ()
_ Uniqueness
_ (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), Monoid as) =>
  Usage ->
  TypeBase dim as ->
  m ()
equalityType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage TypeBase dim as
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
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 as
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 as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase dim as
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 ()
_ Uniqueness
_ (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 as
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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> 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 as dim. Monoid 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), Monoid as) =>
  Usage ->
  BreadCrumbs ->
  TypeBase dim as ->
  m ()
arrayElemTypeWith :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
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 as
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 as dim. Monoid as => TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ TypeBase dim as
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), Monoid as) =>
  Usage ->
  T.Text ->
  TypeBase dim as ->
  m ()
arrayElemType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
arrayElemType Usage
usage Text
desc =
  forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> 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 =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  M.Map Name StructType ->
  M.Map Name StructType ->
  m ()
unifySharedFields :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifyDims 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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound (BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
f]) BreadCrumbs
bcs) StructType
t1 StructType
t2

unifySharedConstructors ::
  MonadUnify m =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  M.Map Name [StructType] ->
  M.Map Name [StructType] ->
  m ()
unifySharedConstructors :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims 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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 ()
_ Uniqueness
_ (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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
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 =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  Name ->
  PatType ->
  m PatType
mustHaveFieldWith :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
mustHaveFieldWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l PatType
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"
  let l_type' :: PatType
l_type' = StructType
l_type forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
  case PatType
t of
    Scalar (TypeVar Aliasing
_ Uniqueness
_ (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 PatType
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 =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 PatType
l_type'
    Scalar (Record Map Name PatType
fields)
      | Just PatType
t' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name PatType
fields -> do
          forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
l_type forall a b. (a -> b) -> a -> b
$ forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t'
          forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
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 PatType
t) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    PatType
_ -> do
      forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
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 PatType
l_type'

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

newDimOnMismatch ::
  (Monoid as, MonadUnify m) =>
  SrcLoc ->
  TypeBase Size as ->
  TypeBase Size as ->
  m (TypeBase Size as, [VName])
newDimOnMismatch :: forall as (m :: * -> *).
(Monoid as, MonadUnify m) =>
SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch SrcLoc
loc TypeBase Size as
t1 TypeBase Size as
t2 = do
  (TypeBase Size as
t, Map (Size, Size) 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 (Size, Size) VName) (t m), MonadTrans t,
 MonadUnify m) =>
p -> Size -> Size -> t m Size
onDims TypeBase Size as
t1 TypeBase Size as
t2) forall a. Monoid a => a
mempty
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size as
t, forall k a. Map k a -> [a]
M.elems Map (Size, Size) VName
seen)
  where
    r :: Rigidity
r = RigidSource -> Rigidity
Rigid forall a b. (a -> b) -> a -> b
$ StructType -> StructType -> RigidSource
RigidCond (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t1) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t2)
    onDims :: p -> Size -> Size -> t m Size
onDims p
_ Size
d1 Size
d2
      | Size
d1 forall a. Eq a => a -> a -> Bool
== Size
d2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
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 (Size
d1, Size
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 -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d
            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 :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
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 (Size
d1, Size
d2) VName
d
              forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d

-- | Like unification, but creates new size variables where mismatches
-- occur.  Returns the new dimensions thus created.
unifyMostCommon ::
  MonadUnify m =>
  Usage ->
  PatType ->
  PatType ->
  m (PatType, [VName])
unifyMostCommon :: forall (m :: * -> *).
MonadUnify m =>
Usage -> PatType -> PatType -> m (PatType, [VName])
unifyMostCommon Usage
usage PatType
t1 PatType
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 =>
UnifyDims 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 (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t1) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t2)
  PatType
t1' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t1
  PatType
t2' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t2
  forall as (m :: * -> *).
(Monoid as, MonadUnify m) =>
SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch (forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) PatType
t1' PatType
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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []

  newDimVar :: SrcLoc -> Rigidity -> Name -> UnifyM VName
newDimVar SrcLoc
loc 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
UnknowableSize SrcLoc
loc 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 Size -> 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)
    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 Size -> 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 ()
expect (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.