{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}

-- | 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.Except
import Control.Monad.State
import Data.Bifunctor
import Data.Char (isAscii)
import Data.List (foldl', intersect)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Util.Pretty hiding (empty)
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
  ppr :: BreadCrumb -> Doc
ppr (MatchingTypes StructType
t1 StructType
t2) =
    Doc
"When matching type"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t1)
      Doc -> Doc -> Doc
</> Doc
"with"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t2)
  ppr (MatchingFields [Name]
fields) =
    Doc
"When matching types of record field"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [Name]
fields) forall a. Semigroup a => a -> a -> a
<> Doc
dot
  ppr (MatchingConstructor Name
c) =
    Doc
"When matching types of constructor" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Name
c) forall a. Semigroup a => a -> a -> a
<> Doc
dot
  ppr (Matching Doc
s) =
    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
  ppr :: BreadCrumbs -> Doc
ppr (BreadCrumbs []) = forall a. Monoid a => a
mempty
  ppr (BreadCrumbs [BreadCrumb]
bcs) = Doc
line forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [BreadCrumb]
bcs)

-- | A usage that caused a type constraint.
data Usage = Usage (Maybe String) 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 -> String -> Usage
mkUsage :: SrcLoc -> String -> Usage
mkUsage = forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe String -> 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 String -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing

instance Pretty Usage where
  ppr :: Usage -> Doc
ppr (Usage Maybe String
Nothing SrcLoc
loc) = Doc
"use at " forall a. Semigroup a => a -> a -> a
<> String -> Doc
textwrap (forall a. Located a => a -> String
locStr SrcLoc
loc)
  ppr (Usage (Just String
s) SrcLoc
loc) = String -> Doc
textwrap String
s Doc -> Doc -> Doc
<+/> Doc
"at" Doc -> Doc -> Doc
<+> String -> Doc
textwrap (forall a. Located a => a -> String
locStr SrcLoc
loc)

instance Located Usage where
  locOf :: Usage -> Loc
locOf (Usage Maybe String
_ 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 (M.Map Name StructType) Usage
  | Equality Usage
  | HasConstrs (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 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 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)) String
  | -- | An existential return size.
    RigidRet (Maybe (QualName VName))
  | RigidLoop
  | -- | Produced by a complicated slice expression.
    RigidSlice (Maybe Size) String
  | -- | Produced by a complicated range expression.
    RigidRange
  | -- | Produced by a range expression with this bound.
    RigidBound String
  | -- | 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"
    Doc -> Doc -> Doc
<+> String -> Doc
text (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"
    Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName VName
fname)
    Doc -> Doc -> Doc
<+> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (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 String
arg) =
  Doc
"is value of argument"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
shorten String
arg)
    Doc -> Doc -> Doc
</> Doc
"passed to"
    Doc -> Doc -> Doc
<+> Doc
fname'
    Doc -> Doc -> Doc
<+> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (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
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" (Doc -> Doc
pquote forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
ppr) Maybe (QualName VName)
fname
prettySource SrcLoc
ctx SrcLoc
loc (RigidSlice Maybe Size
d String
slice) =
  Doc
"is size produced by slice"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
shorten String
slice)
    Doc -> Doc -> Doc
</> Doc
d_desc forall a. Semigroup a => a -> a -> a
<> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (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
d_desc = case Maybe Size
d of
      Just Size
d' -> Doc
"of dimension of size " forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Size
d') forall a. Semigroup a => a -> a -> a
<> Doc
" "
      Maybe Size
Nothing -> forall a. Monoid a => a
mempty
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidLoop =
  Doc
"is unknown size of value returned at" Doc -> Doc -> Doc
<+> String -> Doc
text (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" Doc -> Doc -> Doc
<+> String -> Doc
text (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 String
bound) =
  Doc
"generated from expression"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
shorten String
bound)
    Doc -> Doc -> Doc
</> Doc
"used in range at " forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (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
<> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
v)
    forall a. Semigroup a => a -> a -> a
<> Doc
" going out of scope at "
    forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Doc -> Doc -> Doc
</> Doc
"Originally bound at "
      forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (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"
    Doc -> Doc -> Doc
<+> String -> Doc
text (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
<> String -> Doc
text (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Doc -> Doc -> Doc
</> Doc
"One branch returns array of type: "
      forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr StructType
t1)
    Doc -> Doc -> Doc
</> Doc
"The other an array of type:       "
      forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (forall a. Pretty a => a -> Doc
ppr 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
. forall a. Pretty a => a -> Notes
aNote forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
pretty forall a b. (a -> b) -> a -> b
$
        Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName VName
d) Doc -> Doc -> Doc
<+> 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 (forall a. Pretty a => a -> Notes
aNote forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc
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 -> Doc
note (HasConstrs Map Name [StructType]
cs Usage
_) =
      forall v. IsName v => v -> Doc
pprName VName
v
        Doc -> Doc -> Doc
<+> Doc
"="
        Doc -> Doc -> Doc
<+> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b}. Pretty a => (a, b) -> Doc
ppConstr (forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
        Doc -> Doc -> Doc
<+> Doc
"..."
    note (Overloaded [PrimType]
ts Usage
_) =
      forall v. IsName v => v -> Doc
pprName VName
v Doc -> Doc -> Doc
<+> Doc
"must be one of" Doc -> Doc -> Doc
<+> forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
ts))
    note (HasFields Map Name StructType
fs Usage
_) =
      forall v. IsName v => v -> Doc
pprName VName
v
        Doc -> Doc -> Doc
<+> Doc
"="
        Doc -> Doc -> Doc
<+> Doc -> Doc
braces (forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " (forall a b. (a -> b) -> [a] -> [b]
map forall {v} {b}. IsName v => (v, b) -> Doc
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
ppConstr (a
c, b
_) = Doc
"#" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr a
c Doc -> Doc -> Doc
<+> Doc
"..." Doc -> Doc -> Doc
<+> Doc
"|"
    ppField :: (v, b) -> Doc
ppField (v
f, b
_) = forall v. IsName v => v -> Doc
pprName v
f forall a. Semigroup a => a -> a -> a
<> Doc
":" Doc -> Doc -> Doc
<+> Doc
"..."

-- | 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

-- | 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 (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
fs Map Name StructType
arg_fs) forall a b. (a -> b) -> a -> b
$ \(Name
k, (StructType
k_t1, StructType
k_t2)) -> do
                  let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
k]) BreadCrumbs
bcs
                  Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
k_t1 StructType
k_t2
            | 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:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [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 StructType
a1 (RetType [VName]
b1_dims StructType
b1)),
          Scalar (Arrow ()
_ PName
p2 StructType
a2 (RetType [VName]
b2_dims StructType
b2))
          ) -> 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 String -> 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 a. Semigroup a => a -> a -> a
<>)
            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)) forall a. Semigroup a => a -> a -> a
<>)

            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 -> 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_cs) (forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs)
                        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]
cs) (forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs)
                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 constructors:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"#" forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
ppr) [Name]
missing) forall a. Semigroup a => a -> a -> a
<> Doc
"."
        (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"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Size
d1)
      Doc -> Doc -> Doc
<+> Doc
"and"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Size
d2)
      Doc -> Doc -> Doc
<+> 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"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Size
d1)
          Doc -> Doc -> Doc
<+> Doc
"and"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Size
d2)
          Doc -> Doc -> Doc
<+> 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"
        Doc -> Doc -> Doc
<+> forall v. IsName v => v -> Doc
pprName VName
vn
        Doc -> Doc -> Doc
<+> Doc
"with"
        Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr 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"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
tp)
          Doc -> Doc -> Doc
</> Doc
"with"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
          Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
          Doc -> Doc -> Doc
</> Doc
"This is because"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName v
v)
          Doc -> Doc -> Doc
<+> 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
. Doc -> Doc -> Doc
withIndexLink Doc
"unify-param-existential" forall a b. (a -> b) -> a -> b
$
              Doc
"Parameter(s) "
                forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
pquote forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. IsName v => v -> Doc
pprName) [VName]
problems)
                forall a. Semigroup a => a -> a -> a
<> Doc
" used as size(s) would go out of scope."

  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
      let bcs' :: BreadCrumbs
bcs' =
            BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
              ( Doc -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$
                  Doc
"When verifying that"
                    Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
                    Doc -> Doc -> Doc
<+> String -> Doc
textwrap String
"is not instantiated with a function type, due to"
                    Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr Usage
unlift_usage
              )
              BreadCrumbs
bcs

      m ()
link

      forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs' 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"
            Doc -> Doc -> Doc
<+> forall v. IsName v => v -> Doc
pprName VName
vn
            Doc -> Doc -> Doc
<+> Doc
"cannot be instantiated with type containing anonymous sizes:"
            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
tp)
            Doc -> Doc -> Doc
</> String -> Doc
textwrap String
"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"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"with type"
                  Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
tp)
                  Doc -> Doc -> Doc
</> Doc
"as"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"must be one of"
                  Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
                  Doc -> Doc -> Doc
<+/> Doc
"due to"
                  Doc -> Doc -> Doc
<+/> forall a. Pretty a => a -> Doc
ppr Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Just (HasFields Map Name StructType
required_fields Usage
old_usage) -> do
      m ()
link
      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 bcs' :: BreadCrumbs
bcs' =
                    BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
                      ( Doc -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$
                          forall v. IsName v => v -> Doc
pprName VName
vn
                            Doc -> Doc -> Doc
<+> Doc
"must be a record with at least the fields:"
                            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr (forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields'))
                            Doc -> Doc -> Doc
</> Doc
"due to"
                            Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc
"."
                      )
                      BreadCrumbs
bcs
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') forall a b. (a -> b) -> a -> b
$
                forall k a. Map k a -> [a]
M.elems 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
required_fields Map Name StructType
tp_fields
        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 =>
(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
lvl, Map Name StructType -> Usage -> Constraint
HasFields Map Name StructType
required_fields Usage
old_usage)
        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"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"with type"
              Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
tp)
              Doc -> Doc -> Doc
</> Doc
"as"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"must be a record with fields"
              Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr (forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields))
              Doc -> Doc -> Doc
</> Doc
"due to"
              Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc
"."
    -- See Note [Linking variables to sum types]
    Just (HasConstrs Map Name [StructType]
required_cs Usage
old_usage) ->
      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
        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 Map Name [StructType]
v_cs Usage
_) -> do
              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, Map Name [StructType] -> Usage -> Constraint
HasConstrs Map Name [StructType]
required_cs Usage
old_usage)
          where
            combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs (Int
_, HasConstrs Map Name [StructType]
cs1 Usage
usage1) (a
_, HasConstrs Map Name [StructType]
cs2 Usage
_) =
              (Int
lvl, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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 a. Monoid a => a
mempty
    Maybe Constraint
_ -> m ()
link
  where
    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"

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"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
                  Doc -> Doc -> Doc
<+> Doc
"with"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
                  Doc -> Doc -> Doc
</> Doc
"This is because"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
                  Doc -> Doc -> Doc
<+> 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
$
        String -> Doc
text String
"Cannot unify type"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr StructType
t)
          Doc -> Doc -> Doc
<+> Doc
"with any of " forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [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"
              Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
              Doc -> Doc -> Doc
<+> Doc
"but also one of"
              Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
vn_ts)
              Doc -> Doc -> Doc
<+> Doc
"due to"
              Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr 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 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"
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
            forall a. Semigroup a => a -> a -> a
<> Doc
", but also inferred to be sum type due to"
          Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr Usage
vn_usage
            forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Just (Int
_, HasFields 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"
          Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
            forall a. Semigroup a => a -> a -> a
<> Doc
", but also inferred to be record due to"
          Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr 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" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
ppr [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 " Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
<+> Doc
"does not support equality (is higher-order)."
  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"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t)
                  Doc -> Doc -> Doc
<+> Doc
"does not support equality."
                  Doc -> Doc -> Doc
</> Doc
"Constrained to be higher-order due to"
                  Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr Usage
cusage
                  Doc -> Doc -> Doc
<+> 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 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" Doc -> Doc -> Doc
<+> forall v. IsName v => v -> Doc
pprName VName
vn Doc -> Doc -> Doc
<+> Doc
"does not support equality."

zeroOrderTypeWith ::
  (MonadUnify m, Pretty (Shape dim), Monoid as) =>
  Usage ->
  BreadCrumbs ->
  TypeBase dim as ->
  m ()
zeroOrderTypeWith :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
zeroOrderTypeWith 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" Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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
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"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"at"
              Doc -> Doc -> Doc
<+> String -> Doc
text (forall a. Located a => a -> String
locStr SrcLoc
ploc)
              Doc -> Doc -> Doc
<+> 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, Pretty (Shape dim), Monoid as) =>
  Usage ->
  String ->
  TypeBase dim as ->
  m ()
zeroOrderType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> String -> TypeBase dim as -> m ()
zeroOrderType Usage
usage String
desc =
  forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> 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" Doc -> Doc -> Doc
<+> String -> Doc
textwrap String
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" Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"bound at"
                  Doc -> Doc -> Doc
<+> String -> Doc
text (forall a. Located a => a -> String
locStr SrcLoc
ploc)
                  Doc -> Doc -> Doc
<+> 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 ->
  String ->
  TypeBase dim as ->
  m ()
arrayElemType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> String -> TypeBase dim as -> m ()
arrayElemType Usage
usage String
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" Doc -> Doc -> Doc
<+> String -> Doc
textwrap String
desc

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" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall v. IsName v => v -> Doc
pprName 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 {}) <- 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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs) Usage
usage)
      | Just (Int
lvl, HasConstrs 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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr 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" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> 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" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> 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, Map Name StructType -> Usage -> Constraint
HasFields (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 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, Map Name StructType -> Usage -> Constraint
HasFields (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"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (forall a. Pretty a => a -> Doc
ppr Name
l)
              Doc -> Doc -> Doc
<+> Doc
" of value of type"
              Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
ppr (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 String -> 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 String -> 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. Pretty a => a -> Doc
ppr 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
$ Doc
doc forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
    where
      doc :: Doc
doc =
        Doc
"Types"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t1)
          Doc -> Doc -> Doc
</> Doc
"and"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (forall a. Pretty a => a -> Doc
ppr StructType
t2)
          Doc -> Doc -> Doc
</> Doc
"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 String -> 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 String -> 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 String -> 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.