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 Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Types
data BreadCrumb
= MatchingTypes StructType StructType
| MatchingFields [Name]
| MatchingConstructor Name
| Matching (Doc ())
instance Pretty BreadCrumb where
pretty :: forall ann. BreadCrumb -> Doc ann
pretty (MatchingTypes StructType
t1 StructType
t2) =
Doc ann
"When matching type"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"with"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
pretty (MatchingFields [Name]
fields) =
Doc ann
"When matching types of record field"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
fields) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
pretty (MatchingConstructor Name
c) =
Doc ann
"When matching types of constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
pretty (Matching Doc ()
s) =
forall ann xxx. Doc ann -> Doc xxx
unAnnotate Doc ()
s
newtype BreadCrumbs = BreadCrumbs [BreadCrumb]
noBreadCrumbs :: BreadCrumbs
noBreadCrumbs :: BreadCrumbs
noBreadCrumbs = [BreadCrumb] -> BreadCrumbs
BreadCrumbs []
hasNoBreadCrumbs :: BreadCrumbs -> Bool
hasNoBreadCrumbs :: BreadCrumbs -> Bool
hasNoBreadCrumbs (BreadCrumbs [BreadCrumb]
xs) = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [BreadCrumb]
xs
breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (MatchingFields [Name]
xs) (BreadCrumbs (MatchingFields [Name]
ys : [BreadCrumb]
bcs)) =
[BreadCrumb] -> BreadCrumbs
BreadCrumbs forall a b. (a -> b) -> a -> b
$ [Name] -> BreadCrumb
MatchingFields ([Name]
ys forall a. [a] -> [a] -> [a]
++ [Name]
xs) forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs
breadCrumb BreadCrumb
bc (BreadCrumbs [BreadCrumb]
bcs) =
[BreadCrumb] -> BreadCrumbs
BreadCrumbs forall a b. (a -> b) -> a -> b
$ BreadCrumb
bc forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs
instance Pretty BreadCrumbs where
pretty :: forall ann. BreadCrumbs -> Doc ann
pretty (BreadCrumbs []) = forall a. Monoid a => a
mempty
pretty (BreadCrumbs [BreadCrumb]
bcs) = forall ann. Doc ann
line forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
stack (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [BreadCrumb]
bcs)
data Usage = Usage (Maybe T.Text) SrcLoc
deriving (Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> Usage -> ShowS
Show)
mkUsage :: SrcLoc -> T.Text -> Usage
mkUsage :: SrcLoc -> Text -> Usage
mkUsage = forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Text -> SrcLoc -> Usage
Usage forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
mkUsage' :: SrcLoc -> Usage
mkUsage' :: SrcLoc -> Usage
mkUsage' = Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing
instance Pretty Usage where
pretty :: forall ann. Usage -> Doc ann
pretty (Usage Maybe Text
Nothing SrcLoc
loc) = Doc ann
"use at " forall a. Semigroup a => a -> a -> a
<> forall a. Text -> Doc a
textwrap (forall a. Located a => a -> Text
locText SrcLoc
loc)
pretty (Usage (Just Text
s) SrcLoc
loc) = forall a. Text -> Doc a
textwrap Text
s forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"at" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap (forall a. Located a => a -> Text
locText SrcLoc
loc)
instance Located Usage where
locOf :: Usage -> Loc
locOf (Usage Maybe Text
_ SrcLoc
loc) = forall a. Located a => a -> Loc
locOf SrcLoc
loc
type Level = Int
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
|
Size (Maybe Size) Usage
|
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
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
data RigidSource
=
RigidArg (Maybe (QualName VName)) T.Text
|
RigidRet (Maybe (QualName VName))
| RigidLoop
|
RigidSlice (Maybe Size) T.Text
|
RigidRange
|
RigidBound T.Text
|
RigidCond StructType StructType
|
RigidUnify
| RigidOutOfScope SrcLoc VName
|
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)
data Rigidity = Rigid RigidSource | Nonrigid
deriving (Rigidity -> Rigidity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c== :: Rigidity -> Rigidity -> Bool
Eq, Eq Rigidity
Rigidity -> Rigidity -> Bool
Rigidity -> Rigidity -> Ordering
Rigidity -> Rigidity -> Rigidity
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmax :: Rigidity -> Rigidity -> Rigidity
>= :: Rigidity -> Rigidity -> Bool
$c>= :: Rigidity -> Rigidity -> Bool
> :: Rigidity -> Rigidity -> Bool
$c> :: Rigidity -> Rigidity -> Bool
<= :: Rigidity -> Rigidity -> Bool
$c<= :: Rigidity -> Rigidity -> Bool
< :: Rigidity -> Rigidity -> Bool
$c< :: Rigidity -> Rigidity -> Bool
compare :: Rigidity -> Rigidity -> Ordering
$ccompare :: Rigidity -> Rigidity -> Ordering
Ord, Int -> Rigidity -> ShowS
[Rigidity] -> ShowS
Rigidity -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rigidity] -> ShowS
$cshowList :: [Rigidity] -> ShowS
show :: Rigidity -> String
$cshow :: Rigidity -> String
showsPrec :: Int -> Rigidity -> ShowS
$cshowsPrec :: Int -> Rigidity -> ShowS
Show)
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet Maybe (QualName VName)
Nothing) =
Doc ()
"is unknown size returned by function at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet (Just QualName VName
fname)) =
Doc ()
"is unknown size returned by"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
fname)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidArg Maybe (QualName VName)
fname Text
arg) =
Doc ()
"is value of argument"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
arg))
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"passed to"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann
fname'
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
fname' :: Doc ann
fname' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"function" (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) Maybe (QualName VName)
fname
prettySource SrcLoc
ctx SrcLoc
loc (RigidSlice Maybe Size
d Text
slice) =
Doc ()
"is size produced by slice"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
slice))
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Doc ann
d_desc forall a. Semigroup a => a -> a -> a
<> Doc ()
"at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
d_desc :: Doc ann
d_desc = case Maybe Size
d of
Just Size
d' -> Doc ann
"of dimension of size " forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d') forall a. Semigroup a => a -> a -> a
<> Doc ann
" "
Maybe Size
Nothing -> forall a. Monoid a => a
mempty
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidLoop =
Doc ()
"is unknown size of value returned at" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidRange =
Doc ()
"is unknown length of range at" forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidBound Text
bound) =
Doc ()
"generated from expression"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann xxx. Doc ann -> Doc xxx
shorten (forall a ann. Pretty a => a -> Doc ann
pretty Text
bound))
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"used in range at " forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidOutOfScope SrcLoc
boundloc VName
v) =
Doc ()
"is an unknown size arising from "
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v)
forall a. Semigroup a => a -> a -> a
<> Doc ()
" going out of scope at "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Originally bound at "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
boundloc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidCoerce =
Doc ()
"is an unknown size arising from empty dimension in coercion at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource SrcLoc
_ SrcLoc
_ RigidSource
RigidUnify =
Doc ()
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource SrcLoc
ctx SrcLoc
loc (RigidCond StructType
t1 StructType
t2) =
Doc ()
"is unknown due to conditional expression at "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"One branch returns array of type: "
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"The other an array of type: "
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
dimNotes :: (Located a, MonadUnify m) => a -> Size -> m Notes
dimNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes a
ctx (NamedSize QualName VName
d) = do
Maybe (Int, Constraint)
c <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case Maybe (Int, Constraint)
c of
Just (Int
_, UnknowableSize SrcLoc
loc RigidSource
rsrc) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Notes
aNote forall a b. (a -> b) -> a -> b
$
forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
d) forall a. Doc a -> Doc a -> Doc a
<+> SrcLoc -> SrcLoc -> RigidSource -> Doc ()
prettySource (forall a. Located a => a -> SrcLoc
srclocOf a
ctx) SrcLoc
loc RigidSource
rsrc
Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
dimNotes a
_ Size
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
typeNotes :: (Located a, MonadUnify m) => a -> StructType -> m Notes
typeNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes a
ctx =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Monoid a => [a] -> a
mconcat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes a
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall as. TypeBase Size as -> Set VName
freeInType
typeVarNotes :: MonadUnify m => VName -> m Notes
typeVarNotes :: forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (Doc () -> Notes
aNote forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {ann}. Constraint -> Doc ann
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 ann
note (HasConstrs Map Name [StructType]
cs Usage
_) =
forall v a. IsName v => v -> Doc a
prettyName VName
v
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"="
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {ann}. Pretty a => (a, b) -> Doc ann
ppConstr (forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"..."
note (Overloaded [PrimType]
ts Usage
_) =
forall v a. IsName v => v -> Doc a
prettyName VName
v forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"must be one of" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Monoid a => [a] -> a
mconcat (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts))
note (HasFields Map Name StructType
fs Usage
_) =
forall v a. IsName v => v -> Doc a
prettyName VName
v
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"="
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
braces (forall a. Monoid a => [a] -> a
mconcat (forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
", " (forall a b. (a -> b) -> [a] -> [b]
map forall {v} {b} {a}. IsName v => (v, b) -> Doc a
ppField (forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs))))
note Constraint
_ = forall a. Monoid a => a
mempty
ppConstr :: (a, b) -> Doc ann
ppConstr (a
c, b
_) = Doc ann
"#" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
c forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"..." forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"|"
ppField :: (v, b) -> Doc a
ppField (v
f, b
_) = forall v a. IsName v => v -> Doc a
prettyName v
f forall a. Semigroup a => a -> a -> a
<> Doc a
":" forall a. Doc a -> Doc a -> Doc a
<+> Doc a
"..."
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
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
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
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
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
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
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
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:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Name]
missing) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Size]
targs),
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Size]
arg_targs)
)
| VName
tn forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
targs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
arg_targs -> do
let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching type arguments.") BreadCrumbs
bcs
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Size]
targs [TypeArg Size]
arg_targs
( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v1) []),
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v2) [])
) ->
case (VName -> Maybe Int
nonrigid VName
v1, VName -> Maybe Int
nonrigid VName
v2) of
(Maybe Int
Nothing, Maybe Int
Nothing) -> forall {a}. m a
failure
(Just Int
lvl1, Maybe Int
Nothing) -> Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl1 StructType
t2'
(Maybe Int
Nothing, Just Int
lvl2) -> Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl2 StructType
t1'
(Just Int
lvl1, Just Int
lvl2)
| Int
lvl1 forall a. Ord a => a -> a -> Bool
<= Int
lvl2 -> Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl1 StructType
t2'
| Bool
otherwise -> Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl2 StructType
t1'
(Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v1) []), StructType
_)
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v1 ->
Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl StructType
t2'
(StructType
_, Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v2) []))
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v2 ->
Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl StructType
t1'
( Scalar (Arrow ()
_ PName
p1 StructType
a1 (RetType [VName]
b1_dims StructType
b1)),
Scalar (Arrow ()
_ PName
p2 StructType
a2 (RetType [VName]
b2_dims StructType
b2))
) -> do
let (Constraint
r1, Constraint
r2) =
forall {a}. Bool -> a -> a -> (a, a)
swap
Bool
ord
(Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing forall a. Monoid a => a
mempty)
(SrcLoc -> RigidSource -> Constraint
UnknowableSize forall a. Monoid a => a
mempty RigidSource
RigidUnify)
Int
lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b1_dims forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (Int
lvl, Constraint
r1)) <>)
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b2_dims forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat (Int
lvl, Constraint
r2)) <>)
let bound' :: [VName]
bound' = [VName]
bound forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PName -> Maybe VName
pname [PName
p1, PName
p2] forall a. Semigroup a => a -> a -> a
<> [VName]
b1_dims forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify
(Bool -> Bool
not Bool
ord)
[VName]
bound
(BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching parameter types.") BreadCrumbs
bcs)
StructType
a1
StructType
a2
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify
Bool
ord
[VName]
bound'
(BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching return types.") BreadCrumbs
bcs)
StructType
b1'
StructType
b2'
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') =
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:" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map ((Doc ()
"#" <>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty) [Name]
missing) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
(StructType, StructType)
_
| StructType
t1' forall a. Eq a => a -> a -> Bool
== StructType
t2' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
| Bool
otherwise -> forall {a}. m a
failure
unifyDims :: MonadUnify m => Usage -> UnifyDims m
unifyDims :: forall (m :: * -> *). MonadUnify m => Usage -> UnifyDims m
unifyDims Usage
_ BreadCrumbs
_ [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2
| Size
d1 forall a. Eq a => a -> a -> Bool
== Size
d2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
| Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1 =
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
| Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2 =
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2 = do
Notes
notes <- forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Dimensions"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d1)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"and"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d2)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"do not match."
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 :: 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 ()
onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
| Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1,
Bool -> Bool
not (forall {t :: * -> *}. Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d2) Bool -> Bool -> Bool
|| (VName
d1 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
| Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2,
Bool -> Bool
not (forall {t :: * -> *}. Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d1) Bool -> Bool -> Bool
|| (VName
d2 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
onDims BreadCrumbs
bcs t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2 = do
Notes
notes <- forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Dimensions"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d1)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"and"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Size
d2)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"do not match."
boundParam :: t VName -> Size -> Bool
boundParam t VName
bound (NamedSize (QualName [VName]
_ VName
d)) = VName
d forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound
boundParam t VName
_ Size
_ = Bool
False
occursCheck ::
MonadUnify m =>
Usage ->
BreadCrumbs ->
VName ->
StructType ->
m ()
occursCheck :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp =
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
vn forall a. Ord a => a -> Set a -> Bool
`S.member` forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars StructType
tp) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Occurs check: cannot instantiate"
forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
scopeCheck ::
MonadUnify m =>
Usage ->
BreadCrumbs ->
VName ->
Level ->
StructType ->
m ()
scopeCheck :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
vn Int
max_lvl StructType
tp = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
forall {m :: * -> *} {as}.
(MonadUnify m, Monoid as) =>
Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints StructType
tp
where
checkType :: Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints TypeBase Size as
t =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
check Constraints
constraints) forall a b. (a -> b) -> a -> b
$ forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size as
t forall a. Semigroup a => a -> a -> a
<> forall as. TypeBase Size as -> Set VName
freeInType TypeBase Size as
t
check :: Constraints -> VName -> m ()
check Constraints
constraints VName
v
| Just (Int
lvl, Constraint
c) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints,
Int
lvl forall a. Ord a => a -> a -> Bool
> Int
max_lvl =
if Constraint -> Bool
rigidConstraint Constraint
c
then forall {m :: * -> *} {v} {b}. (MonadUnify m, IsName v) => v -> m b
scopeViolation VName
v
else forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
max_lvl, Constraint
c)
| Bool
otherwise =
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
scopeViolation :: v -> m b
scopeViolation v
v = do
Notes
notes <- forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes Usage
usage StructType
tp
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify type"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"with"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"(scope violation)."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"This is because"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName v
v)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is rigidly bound in a deeper scope."
linkVarToType ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
VName ->
Level ->
StructType ->
m ()
linkVarToType :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs VName
vn Int
lvl StructType
tp_unnorm = do
StructType
tp <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
tp_unnorm
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
vn Int
lvl StructType
tp
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let link :: m ()
link = do
let (Set VName
witnessed, Set VName
not_witnessed) = StructType -> (Set VName, Set VName)
determineSizeWitnesses StructType
tp
used :: VName -> Bool
used VName
v = VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
witnessed Bool -> Bool -> Bool
|| VName
v forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
not_witnessed
ext :: [VName]
ext = forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
used [VName]
bound
case forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set VName
witnessed) [VName]
ext of
[] ->
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp) Usage
usage)
[VName]
problems ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-param-existential" forall a b. (a -> b) -> a -> b
$
Doc ()
"Parameter(s) "
forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map (forall ann. Doc ann -> Doc ann
dquotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v a. IsName v => v -> Doc a
prettyName) [VName]
problems)
forall a. Semigroup a => a -> a -> a
<> Doc ()
" used as size(s) would go out of scope."
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"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
"is not instantiated with a function type, due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty 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"
forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"cannot be instantiated with type containing anonymous sizes:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
forall a. Doc a -> Doc a -> Doc a
</> forall a. Text -> Doc a
textwrap Text
"This is usually because the size of an array returned by a higher-order function argument cannot be determined statically. This can also be due to the return size being a value parameter. Add type annotation to clarify."
Just (Equality Usage
_) -> do
m ()
link
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage StructType
tp
Just (Overloaded [PrimType]
ts Usage
old_usage)
| StructType
tp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. PrimType -> ScalarTypeBase dim as
Prim) [PrimType]
ts -> do
m ()
link
case StructType
tp of
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v) [])
| Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints ->
forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
StructType
_ ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot instantiate"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (HasFields 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 a. IsName v => v -> Doc a
prettyName VName
vn
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be a record with at least the fields:"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields'))
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
)
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"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
tp)
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be a record with fields"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields))
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
old_usage forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
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
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"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
dim')
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"(scope violation)."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"This is because"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
dim')
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is rigidly bound in a deeper scope."
Constraint
_ -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (forall vn. QualName vn -> vn
qualLeaf QualName VName
dim') (Int
lvl, Constraint
c)
Size
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Maybe Size -> Usage -> Constraint
Size (forall a. a -> Maybe a
Just Size
dim) Usage
usage)
mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m ()
mustBeOneOf :: forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType
req_t] Usage
usage StructType
t = forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
req_t)) StructType
t
mustBeOneOf [PrimType]
ts Usage
usage StructType
t = do
StructType
t' <- forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let isRigid' :: VName -> Bool
isRigid' VName
v = VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints
case StructType
t' of
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v) [])
| Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ VName -> Bool
isRigid' VName
v -> forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
Scalar (Prim PrimType
pt) | PrimType
pt forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ts -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
StructType
_ -> forall {a}. m a
failure
where
failure :: m a
failure =
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify type"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with any of " forall a. Semigroup a => a -> a -> a
<> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
linkVarToTypes :: MonadUnify m => Usage -> VName -> [PrimType] -> m ()
linkVarToTypes :: forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
vn [PrimType]
ts = do
Maybe (Int, Constraint)
vn_constraint <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case Maybe (Int, Constraint)
vn_constraint of
Just (Int
lvl, Overloaded [PrimType]
vn_ts Usage
vn_usage) ->
case [PrimType]
ts forall a. Eq a => [a] -> [a] -> [a]
`intersect` [PrimType]
vn_ts of
[] ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"but also one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
vn_ts)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
[PrimType]
ts' -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts' Usage
usage)
Just (Int
_, HasConstrs Map Name [StructType]
_ Usage
vn_usage) ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be sum type due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (Int
_, HasFields Map Name StructType
_ Usage
vn_usage) ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be record due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
vn_usage
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (Int
lvl, Constraint
_) -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts Usage
usage)
Maybe (Int, Constraint)
Nothing ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot constrain type to one of" forall a. Doc a -> Doc a -> Doc a
<+> forall a. [Doc a] -> Doc a
commasep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [PrimType]
ts)
equalityType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
TypeBase dim as ->
m ()
equalityType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage TypeBase dim as
t = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type " forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim as
t) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality (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"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim as
t)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Constrained to be higher-order due to"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty Usage
cusage
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
| Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Usage -> Constraint
Equality Usage
usage)
Just (Int
_, Overloaded [PrimType]
_ Usage
_) ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
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" forall a. Doc a -> Doc a -> Doc a
<+> forall v a. IsName v => v -> Doc a
prettyName VName
vn forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."
zeroOrderTypeWith ::
(MonadUnify m, 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" forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim as
t) forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ TypeBase dim as
t
where
mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted Usage
usage)
Just (Int
_, ParamType Liftedness
Lifted SrcLoc
ploc) ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type parameter"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> String
locStr SrcLoc
ploc)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"may be a function."
Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
zeroOrderType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
T.Text ->
TypeBase dim as ->
m ()
zeroOrderType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType Usage
usage Text
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" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
desc
arrayElemTypeWith ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
BreadCrumbs ->
TypeBase dim as ->
m ()
arrayElemTypeWith :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type" forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase dim as
t) forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars forall a b. (a -> b) -> a -> b
$ TypeBase dim as
t
where
mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted Usage
usage)
Just (Int
_, ParamType Liftedness
l SrcLoc
ploc)
| Liftedness
l forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Liftedness
Lifted, Liftedness
SizeLifted] ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Type parameter"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
vn)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"bound at"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> String
locStr SrcLoc
ploc)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is lifted and cannot be an array element."
Maybe (Int, Constraint)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
arrayElemType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
T.Text ->
TypeBase dim as ->
m ()
arrayElemType :: forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
arrayElemType Usage
usage Text
desc =
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage forall a b. (a -> b) -> a -> b
$ BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb BreadCrumb
bc BreadCrumbs
noBreadCrumbs
where
bc :: BreadCrumb
bc = Doc () -> BreadCrumb
Matching forall a b. (a -> b) -> a -> b
$ Doc ()
"When checking" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Text -> Doc a
textwrap Text
desc
unifySharedConstructors ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
M.Map Name [StructType] ->
M.Map Name [StructType] ->
m ()
unifySharedConstructors :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs1 Map Name [StructType]
cs2 =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [StructType]
cs1 Map Name [StructType]
cs2) forall a b. (a -> b) -> a -> b
$ \(Name
c, ([StructType]
f1, [StructType]
f2)) ->
Name -> [StructType] -> [StructType] -> m ()
unifyConstructor Name
c [StructType]
f1 [StructType]
f2
where
unifyConstructor :: Name -> [StructType] -> [StructType] -> m ()
unifyConstructor Name
c [StructType]
f1 [StructType]
f2
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f2 = do
let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Name -> BreadCrumb
MatchingConstructor Name
c) BreadCrumbs
bcs
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') [StructType]
f1 [StructType]
f2
| Bool
otherwise =
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
bcs forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName Name
c) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
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" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Scalar (Sum Map Name [StructType]
cs) ->
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
c Map Name [StructType]
cs of
Maybe [StructType]
Nothing ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Constuctor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"not present in type."
Just [StructType]
fs'
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs' -> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage) [StructType]
fs [StructType]
fs'
| Bool
otherwise ->
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs forall a b. (a -> b) -> a -> b
$
Doc ()
"Different arity for constructor" forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
c) forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
StructType
_ ->
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs
mustHaveFieldWith ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
Name ->
PatType ->
m PatType
mustHaveFieldWith :: forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
mustHaveFieldWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l PatType
t = do
Constraints
constraints <- forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
StructType
l_type <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Name
"t"
let l_type' :: PatType
l_type' = StructType
l_type forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
case PatType
t of
Scalar (TypeVar Aliasing
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [])
| Just (Int
lvl, NoConstraint {}) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
tn Int
lvl StructType
l_type
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, 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"
forall a. Doc a -> Doc a -> Doc a
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
l)
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
" of value of type"
forall a. Doc a -> Doc a -> Doc a
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall dim as. TypeBase dim as -> TypeBase () ()
toStructural PatType
t) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
PatType
_ -> do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
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
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
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
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'
type UnifyMState = (Constraints, Int)
newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
deriving
( Applicative UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> UnifyM a
$creturn :: forall a. a -> UnifyM a
>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
Monad,
forall a b. a -> UnifyM b -> UnifyM a
forall a b. (a -> b) -> UnifyM a -> UnifyM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> UnifyM b -> UnifyM a
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
fmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
Functor,
Functor UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
liftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
pure :: forall a. a -> UnifyM a
$cpure :: forall a. a -> UnifyM a
Applicative,
MonadState UnifyMState,
MonadError TypeError
)
newVar :: Name -> UnifyM VName
newVar :: Name -> UnifyM VName
newVar Name
name = do
(Constraints
x, Int
i) <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Constraints
x, Int
i forall a. Num a => a -> a -> a
+ Int
1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> Int -> VName
VName (Name -> Int -> Name
mkTypeVarName Name
name Int
i) Int
i
instance MonadUnify UnifyM where
getConstraints :: UnifyM Constraints
getConstraints = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a, b) -> a
fst
putConstraints :: Constraints -> UnifyM ()
putConstraints Constraints
x = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \(Constraints
_, Int
i) -> (Constraints
x, Int
i)
newTypeVar :: forall als dim.
Monoid als =>
SrcLoc -> Name -> UnifyM (TypeBase dim als)
newTypeVar SrcLoc
loc Name
name = do
VName
v <- Name -> UnifyM VName
newVar Name
name
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Lifted forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []
newDimVar :: SrcLoc -> Rigidity -> Name -> UnifyM VName
newDimVar SrcLoc
loc Rigidity
rigidity Name
name = do
VName
dim <- Name -> UnifyM VName
newVar Name
name
case Rigidity
rigidity of
Rigid RigidSource
src -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
loc RigidSource
src)
Rigidity
Nonrigid -> forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim
curLevel :: UnifyM Int
curLevel = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc ()
doc =
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ Doc ()
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
matchError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 =
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann
doc forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty BreadCrumbs
bcs
where
doc :: Doc a
doc =
Doc a
"Types"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t1)
forall a. Doc a -> Doc a -> Doc a
</> Doc a
"and"
forall a. Doc a -> Doc a -> Doc a
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a ann. Pretty a => a -> Doc ann
pretty StructType
t2)
forall a. Doc a -> Doc a -> Doc a
</> Doc a
"do not match."
runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM :: forall a.
[TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams (UnifyM StateT (Constraints, Int) (Except TypeError) a
m) =
forall e a. Except e a -> Either e a
runExcept forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (Constraints, Int) (Except TypeError) a
m (Constraints
constraints, Int
0)
where
constraints :: Constraints
constraints =
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
nonrigid [TypeParam]
nonrigid_tparams forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
rigid [TypeParam]
rigid_tparams
nonrigid :: TypeParamBase a -> (a, (a, Constraint))
nonrigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, Maybe Size -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc))
nonrigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
l forall a b. (a -> b) -> a -> b
$ Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing SrcLoc
loc))
rigid :: TypeParamBase a -> (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, SrcLoc -> Constraint
ParamSize SrcLoc
loc))
rigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc))
doUnification ::
Loc ->
[TypeParam] ->
[TypeParam] ->
StructType ->
StructType ->
Either TypeError StructType
doUnification :: Loc
-> [TypeParam]
-> [TypeParam]
-> StructType
-> StructType
-> Either TypeError StructType
doUnification Loc
loc [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams StructType
t1 StructType
t2 =
forall a.
[TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
expect (Maybe Text -> SrcLoc -> Usage
Usage forall a. Maybe a
Nothing (forall a. Located a => a -> SrcLoc
srclocOf Loc
loc)) StructType
t1 StructType
t2
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2