module Language.Futhark.TypeChecker.Unify
( Constraint (..),
Usage (..),
mkUsage,
mkUsage',
Level,
Constraints,
MonadUnify (..),
Rigidity (..),
RigidSource (..),
BreadCrumbs,
noBreadCrumbs,
hasNoBreadCrumbs,
dimNotes,
zeroOrderType,
arrayElemType,
mustHaveConstr,
mustHaveField,
mustBeOneOf,
equalityType,
normType,
normTypeFully,
unify,
unifyMostCommon,
doUnification,
)
where
import Control.Monad
import Control.Monad.Except
import Control.Monad.State
import Data.List (foldl', intersect)
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Types
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"
Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1)
Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Doc ann
"with"
Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t2)
pretty (MatchingFields [Name]
fields) =
Doc ann
"When matching types of record field"
Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes ([Doc ann] -> Doc ann
forall a. Monoid a => [a] -> a
mconcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"." ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc ann) -> [Name] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty [Name]
fields)
Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
dot
pretty (MatchingConstructor Name
c) =
Doc ann
"When matching types of constructor" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
c) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
dot
pretty (Matching Doc ()
s) =
Doc () -> Doc ann
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) = [BreadCrumb] -> Bool
forall a. [a] -> Bool
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 ([BreadCrumb] -> BreadCrumbs) -> [BreadCrumb] -> BreadCrumbs
forall a b. (a -> b) -> a -> b
$ [Name] -> BreadCrumb
MatchingFields ([Name]
ys [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
xs) BreadCrumb -> [BreadCrumb] -> [BreadCrumb]
forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs
breadCrumb BreadCrumb
bc (BreadCrumbs [BreadCrumb]
bcs) =
[BreadCrumb] -> BreadCrumbs
BreadCrumbs ([BreadCrumb] -> BreadCrumbs) -> [BreadCrumb] -> BreadCrumbs
forall a b. (a -> b) -> a -> b
$ BreadCrumb
bc BreadCrumb -> [BreadCrumb] -> [BreadCrumb]
forall a. a -> [a] -> [a]
: [BreadCrumb]
bcs
instance Pretty BreadCrumbs where
pretty :: forall ann. BreadCrumbs -> Doc ann
pretty (BreadCrumbs []) = Doc ann
forall a. Monoid a => a
mempty
pretty (BreadCrumbs [BreadCrumb]
bcs) = Doc ann
forall ann. Doc ann
line Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall a. [Doc a] -> Doc a
stack ((BreadCrumb -> Doc ann) -> [BreadCrumb] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map BreadCrumb -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumb -> Doc ann
pretty [BreadCrumb]
bcs)
data Usage = Usage (Maybe T.Text) Loc
deriving (Int -> Usage -> ShowS
[Usage] -> ShowS
Usage -> String
(Int -> Usage -> ShowS)
-> (Usage -> String) -> ([Usage] -> ShowS) -> Show Usage
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Usage -> ShowS
showsPrec :: Int -> Usage -> ShowS
$cshow :: Usage -> String
show :: Usage -> String
$cshowList :: [Usage] -> ShowS
showList :: [Usage] -> ShowS
Show)
mkUsage :: (Located a) => a -> T.Text -> Usage
mkUsage :: forall a. Located a => a -> Text -> Usage
mkUsage = (Text -> Loc -> Usage) -> Loc -> Text -> Usage
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Text -> Loc -> Usage
Usage (Maybe Text -> Loc -> Usage)
-> (Text -> Maybe Text) -> Text -> Loc -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Maybe Text
forall a. a -> Maybe a
Just) (Loc -> Text -> Usage) -> (a -> Loc) -> a -> Text -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Loc
forall a. Located a => a -> Loc
locOf
mkUsage' :: (Located a) => a -> Usage
mkUsage' :: forall a. Located a => a -> Usage
mkUsage' = Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> (a -> Loc) -> a -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Loc
forall a. Located a => a -> Loc
locOf
instance Pretty Usage where
pretty :: forall ann. Usage -> Doc ann
pretty (Usage Maybe Text
Nothing Loc
loc) = Doc ann
"use at " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall a. Text -> Doc a
textwrap (Loc -> Text
forall a. Located a => a -> Text
locText Loc
loc)
pretty (Usage (Just Text
s) Loc
loc) = Text -> Doc ann
forall a. Text -> Doc a
textwrap Text
s Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"at" Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Text -> Doc ann
forall a. Text -> Doc a
textwrap (Loc -> Text
forall a. Located a => a -> Text
locText Loc
loc)
instance Located Usage where
locOf :: Usage -> Loc
locOf (Usage Maybe Text
_ Loc
loc) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc
type Level = Int
data Constraint
= NoConstraint Liftedness Usage
| ParamType Liftedness Loc
| Constraint StructRetType Usage
| Overloaded [PrimType] Usage
| HasFields Liftedness (M.Map Name StructType) Usage
| Equality Usage
| HasConstrs Liftedness (M.Map Name [StructType]) Usage
| ParamSize Loc
|
Size (Maybe Exp) Usage
|
UnknownSize Loc RigidSource
deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show)
instance Located Constraint where
locOf :: Constraint -> Loc
locOf (NoConstraint Liftedness
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (ParamType Liftedness
_ Loc
usage) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
usage
locOf (Constraint StructRetType
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (Overloaded [PrimType]
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (HasFields Liftedness
_ Map Name StructType
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (Equality Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (HasConstrs Liftedness
_ Map Name [StructType]
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (ParamSize Loc
loc) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc
locOf (Size Maybe Exp
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (UnknownSize Loc
loc RigidSource
_) = Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc
type Constraints = M.Map VName (Level, Constraint)
lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst VName
v Constraints
constraints = case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
Just (Constraint StructRetType
t Usage
_) -> Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just (Subst StructRetType -> Maybe (Subst StructRetType))
-> Subst StructRetType -> Maybe (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ [TypeParam] -> StructRetType -> Subst StructRetType
forall t. [TypeParam] -> t -> Subst t
Subst [] (StructRetType -> Subst StructRetType)
-> StructRetType -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ TypeSubs -> StructRetType -> StructRetType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) StructRetType
t
Just (Size (Just Exp
d) Usage
_) ->
Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just (Subst StructRetType -> Maybe (Subst StructRetType))
-> Subst StructRetType -> Maybe (Subst StructRetType)
forall a b. (a -> b) -> a -> b
$ Exp -> Subst StructRetType
forall t. Exp -> Subst t
ExpSubst (Exp -> Subst StructRetType) -> Exp -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d
Maybe Constraint
_ -> Maybe (Subst StructRetType)
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 Loc VName
|
RigidCoerce
deriving (RigidSource -> RigidSource -> Bool
(RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool) -> Eq RigidSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RigidSource -> RigidSource -> Bool
== :: RigidSource -> RigidSource -> Bool
$c/= :: RigidSource -> RigidSource -> Bool
/= :: RigidSource -> RigidSource -> Bool
Eq, Eq RigidSource
Eq RigidSource
-> (RigidSource -> RigidSource -> Ordering)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> RigidSource)
-> (RigidSource -> RigidSource -> RigidSource)
-> Ord RigidSource
RigidSource -> RigidSource -> Bool
RigidSource -> RigidSource -> Ordering
RigidSource -> RigidSource -> RigidSource
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RigidSource -> RigidSource -> Ordering
compare :: RigidSource -> RigidSource -> Ordering
$c< :: RigidSource -> RigidSource -> Bool
< :: RigidSource -> RigidSource -> Bool
$c<= :: RigidSource -> RigidSource -> Bool
<= :: RigidSource -> RigidSource -> Bool
$c> :: RigidSource -> RigidSource -> Bool
> :: RigidSource -> RigidSource -> Bool
$c>= :: RigidSource -> RigidSource -> Bool
>= :: RigidSource -> RigidSource -> Bool
$cmax :: RigidSource -> RigidSource -> RigidSource
max :: RigidSource -> RigidSource -> RigidSource
$cmin :: RigidSource -> RigidSource -> RigidSource
min :: RigidSource -> RigidSource -> RigidSource
Ord, Int -> RigidSource -> ShowS
[RigidSource] -> ShowS
RigidSource -> String
(Int -> RigidSource -> ShowS)
-> (RigidSource -> String)
-> ([RigidSource] -> ShowS)
-> Show RigidSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RigidSource -> ShowS
showsPrec :: Int -> RigidSource -> ShowS
$cshow :: RigidSource -> String
show :: RigidSource -> String
$cshowList :: [RigidSource] -> ShowS
showList :: [RigidSource] -> ShowS
Show)
data Rigidity = Rigid RigidSource | Nonrigid
deriving (Rigidity -> Rigidity -> Bool
(Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool) -> Eq Rigidity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
/= :: Rigidity -> Rigidity -> Bool
Eq, Eq Rigidity
Eq Rigidity
-> (Rigidity -> Rigidity -> Ordering)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Rigidity)
-> (Rigidity -> Rigidity -> Rigidity)
-> Ord Rigidity
Rigidity -> Rigidity -> Bool
Rigidity -> Rigidity -> Ordering
Rigidity -> Rigidity -> Rigidity
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Rigidity -> Rigidity -> Ordering
compare :: Rigidity -> Rigidity -> Ordering
$c< :: Rigidity -> Rigidity -> Bool
< :: Rigidity -> Rigidity -> Bool
$c<= :: Rigidity -> Rigidity -> Bool
<= :: Rigidity -> Rigidity -> Bool
$c> :: Rigidity -> Rigidity -> Bool
> :: Rigidity -> Rigidity -> Bool
$c>= :: Rigidity -> Rigidity -> Bool
>= :: Rigidity -> Rigidity -> Bool
$cmax :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
min :: Rigidity -> Rigidity -> Rigidity
Ord, Int -> Rigidity -> ShowS
[Rigidity] -> ShowS
Rigidity -> String
(Int -> Rigidity -> ShowS)
-> (Rigidity -> String) -> ([Rigidity] -> ShowS) -> Show Rigidity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Rigidity -> ShowS
showsPrec :: Int -> Rigidity -> ShowS
$cshow :: Rigidity -> String
show :: Rigidity -> String
$cshowList :: [Rigidity] -> ShowS
showList :: [Rigidity] -> ShowS
Show)
prettySource :: Loc -> Loc -> RigidSource -> Doc ()
prettySource :: Loc -> Loc -> RigidSource -> Doc ()
prettySource Loc
ctx Loc
loc (RigidRet Maybe (QualName VName)
Nothing) =
Doc ()
"is unknown size returned by function at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidRet (Just QualName VName
fname)) =
Doc ()
"is unknown size returned by"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
fname)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidArg Maybe (QualName VName)
fname Text
arg) =
Doc ()
"is value of argument"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc ()
forall ann xxx. Doc ann -> Doc xxx
shorten (Text -> Doc Any
forall a. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
arg))
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"passed to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
forall ann. Doc ann
fname'
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
fname' :: Doc ann
fname' = Doc ann
-> (QualName VName -> Doc ann) -> Maybe (QualName VName) -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
"function" (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann)
-> (QualName VName -> Doc ann) -> QualName VName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty) Maybe (QualName VName)
fname
prettySource Loc
ctx Loc
loc (RigidSlice Maybe Exp
d Text
slice) =
Doc ()
"is size produced by slice"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc ()
forall ann xxx. Doc ann -> Doc xxx
shorten (Text -> Doc Any
forall a. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
slice))
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
forall ann. Doc ann
d_desc
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
d_desc :: Doc ann
d_desc = case Maybe Exp
d of
Just Exp
d' -> Doc ann
"of dimension of size " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
d') Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" "
Maybe Exp
Nothing -> Doc ann
forall a. Monoid a => a
mempty
prettySource Loc
ctx Loc
loc RigidSource
RigidLoop =
Doc ()
"is unknown size of value returned at" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc RigidSource
RigidRange =
Doc ()
"is unknown length of range at" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidBound Text
bound) =
Doc ()
"generated from expression"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc Any -> Doc ()
forall ann xxx. Doc ann -> Doc xxx
shorten (Text -> Doc Any
forall a. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
bound))
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"used in range at "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc (RigidOutOfScope Loc
boundloc VName
v) =
Doc ()
"is an unknown size arising from "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" going out of scope at "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Originally bound at "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
boundloc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
ctx Loc
loc RigidSource
RigidCoerce =
Doc ()
"is an unknown size arising from empty dimension in coercion at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
prettySource Loc
_ Loc
_ RigidSource
RigidUnify =
Doc ()
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource Loc
ctx Loc
loc (RigidCond StructType
t1 StructType
t2) =
Doc ()
"is unknown due to conditional expression at "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> Loc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel Loc
ctx Loc
loc)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"One branch returns array of type: "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"The other an array of type: "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
align (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t2)
dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes
dimNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes a
ctx (Var QualName VName
d Info StructType
_ SrcLoc
_) = do
Maybe (Int, Constraint)
c <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) (Constraints -> Maybe (Int, Constraint))
-> m Constraints -> m (Maybe (Int, Constraint))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case Maybe (Int, Constraint)
c of
Just (Int
_, UnknownSize Loc
loc RigidSource
rsrc) ->
Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Notes -> m Notes) -> (Doc () -> Notes) -> Doc () -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Notes
aNote (Doc () -> m Notes) -> Doc () -> m Notes
forall a b. (a -> b) -> a -> b
$
Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty QualName VName
d) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Loc -> Loc -> RigidSource -> Doc ()
prettySource (a -> Loc
forall a. Located a => a -> Loc
locOf a
ctx) Loc
loc RigidSource
rsrc
Maybe (Int, Constraint)
_ -> Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty
dimNotes a
_ Exp
_ = Notes -> m Notes
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty
typeNotes :: (Located a, MonadUnify m) => a -> StructType -> m Notes
typeNotes :: forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes a
ctx =
([Notes] -> Notes) -> m [Notes] -> m Notes
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Notes] -> Notes
forall a. Monoid a => [a] -> a
mconcat
(m [Notes] -> m Notes)
-> (StructType -> m [Notes]) -> StructType -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> m Notes) -> [VName] -> m [Notes]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (a -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes a
ctx (Exp -> m Notes) -> (VName -> Exp) -> VName -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualName VName -> SrcLoc -> Exp)
-> SrcLoc -> QualName VName -> Exp
forall a b c. (a -> b -> c) -> b -> a -> c
flip QualName VName -> SrcLoc -> Exp
sizeFromName SrcLoc
forall a. Monoid a => a
mempty (QualName VName -> Exp)
-> (VName -> QualName VName) -> VName -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> QualName VName
forall v. v -> QualName v
qualName)
([VName] -> m [Notes])
-> (StructType -> [VName]) -> StructType -> m [Notes]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set VName -> [VName]
forall a. Set a -> [a]
S.toList
(Set VName -> [VName])
-> (StructType -> Set VName) -> StructType -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FV -> Set VName
fvVars
(FV -> Set VName) -> (StructType -> FV) -> StructType -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StructType -> FV
forall u. TypeBase Exp u -> FV
freeInType
typeVarNotes :: (MonadUnify m) => VName -> m Notes
typeVarNotes :: forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v = Notes
-> ((Int, Constraint) -> Notes) -> Maybe (Int, Constraint) -> Notes
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Notes
forall a. Monoid a => a
mempty (Constraint -> Notes
note (Constraint -> Notes)
-> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd) (Maybe (Int, Constraint) -> Notes)
-> (Constraints -> Maybe (Int, Constraint)) -> Constraints -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v (Constraints -> Notes) -> m Constraints -> m Notes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
where
note :: Constraint -> Notes
note (HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
_) =
Doc () -> Notes
aNote (Doc () -> Notes) -> Doc () -> Notes
forall a b. (a -> b) -> a -> b
$
VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"="
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
hsep (((Name, [StructType]) -> Doc ())
-> [(Name, [StructType])] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [StructType]) -> Doc ()
forall {a} {b} {ann}. Pretty a => (a, b) -> Doc ann
ppConstr (Map Name [StructType] -> [(Name, [StructType])]
forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"..."
note (Overloaded [PrimType]
ts Usage
_) =
Doc () -> Notes
aNote (Doc () -> Notes) -> Doc () -> Notes
forall a b. (a -> b) -> a -> b
$ VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be one of" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. Monoid a => [a] -> a
mconcat (Doc () -> [Doc ()] -> [Doc ()]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ()
", " ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts))
note (HasFields Liftedness
_ Map Name StructType
fs Usage
_) =
Doc () -> Notes
aNote (Doc () -> Notes) -> Doc () -> Notes
forall a b. (a -> b) -> a -> b
$
VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
v
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"="
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
braces ([Doc ()] -> Doc ()
forall a. Monoid a => [a] -> a
mconcat (Doc () -> [Doc ()] -> [Doc ()]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ()
", " (((Name, StructType) -> Doc ()) -> [(Name, StructType)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Name, StructType) -> Doc ()
forall {v} {b} {a}. IsName v => (v, b) -> Doc a
ppField (Map Name StructType -> [(Name, StructType)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs))))
note Constraint
_ = Notes
forall a. Monoid a => a
mempty
ppConstr :: (a, b) -> Doc ann
ppConstr (a
c, b
_) = Doc ann
"#" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
c Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"..." Doc ann -> Doc ann -> Doc ann
forall a. Doc a -> Doc a -> Doc a
<+> Doc ann
"|"
ppField :: (v, b) -> Doc a
ppField (v
f, b
_) = v -> Doc a
forall a. v -> Doc a
forall v a. IsName v => v -> Doc a
prettyName v
f Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
":" Doc a -> Doc 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 <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
Constraints -> m ()
forall (m :: * -> *). MonadUnify m => Constraints -> m ()
putConstraints (Constraints -> m ()) -> Constraints -> m ()
forall a b. (a -> b) -> a -> b
$ Constraints -> Constraints
f Constraints
x
newTypeVar :: (Monoid als, Located a) => a -> Name -> m (TypeBase dim als)
newDimVar :: Usage -> Rigidity -> Name -> m VName
newRigidDim :: (Located a) => a -> RigidSource -> Name -> m VName
newRigidDim a
loc = Usage -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar (a -> Usage
forall a. Located a => a -> Usage
mkUsage' a
loc) (Rigidity -> Name -> m VName)
-> (RigidSource -> Rigidity) -> RigidSource -> Name -> m VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RigidSource -> Rigidity
Rigid
newFlexibleDim :: Usage -> Name -> m VName
newFlexibleDim Usage
usage = Usage -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
Usage -> Rigidity -> Name -> m VName
newDimVar Usage
usage Rigidity
Nonrigid
curLevel :: m Level
matchError ::
(Located loc) =>
loc ->
Notes ->
BreadCrumbs ->
StructType ->
StructType ->
m a
unifyError ::
(Located loc) =>
loc ->
Notes ->
BreadCrumbs ->
Doc () ->
m a
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 <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ TypeSubs -> a -> a
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 NoUniqueness
_ (QualName [] VName
v) [])) = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
Just (Constraint (RetType [] StructType
t') Usage
_) -> StructType -> m StructType
forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t'
Maybe Constraint
_ -> StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
normType StructType
t = StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
rigidConstraint :: Constraint -> Bool
rigidConstraint :: Constraint -> Bool
rigidConstraint ParamType {} = Bool
True
rigidConstraint ParamSize {} = Bool
True
rigidConstraint UnknownSize {} = Bool
True
rigidConstraint Constraint
_ = Bool
False
unsharedConstructorsMsg :: M.Map Name t -> M.Map Name t -> Doc a
unsharedConstructorsMsg :: forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name t
cs1 Map Name t
cs2 =
Doc a
"Unshared constructors:" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
commasep ((Name -> Doc a) -> [Name] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc a
"#" <>) (Doc a -> Doc a) -> (Name -> Doc a) -> Name -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty) [Name]
missing) Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
"."
where
missing :: [Name]
missing =
(Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs1) (Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs2)
[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs2) (Map Name t -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name t
cs1)
isRigid :: VName -> Constraints -> Bool
isRigid :: VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints =
Bool
-> ((Int, Constraint) -> Bool) -> Maybe (Int, Constraint) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Constraint -> Bool
rigidConstraint (Constraint -> Bool)
-> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd) (Maybe (Int, Constraint) -> Bool)
-> Maybe (Int, Constraint) -> Bool
forall a b. (a -> b) -> a -> b
$ VName -> Constraints -> Maybe (Int, Constraint)
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) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Constraint -> Bool
rigidConstraint Constraint
c
Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl
type UnifySizes m =
BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Exp -> Exp -> m ()
flipUnifySizes :: UnifySizes m -> UnifySizes m
flipUnifySizes :: forall (m :: * -> *). UnifySizes m -> UnifySizes m
flipUnifySizes UnifySizes m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
t1 Exp
t2 =
UnifySizes m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
t2 Exp
t1
unifyWith ::
(MonadUnify m) =>
UnifySizes m ->
Usage ->
[VName] ->
BreadCrumbs ->
StructType ->
StructType ->
m ()
unifyWith :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage = Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
False
where
swap :: Bool -> a -> a -> (a, a)
swap Bool
True a
x a
y = (a
y, a
x)
swap Bool
False a
x a
y = (a
x, a
y)
subunify :: Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs StructType
t1 StructType
t2 = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
StructType
t1' <- StructType -> m StructType
forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t1
StructType
t2' <- StructType -> m StructType
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 = SrcLoc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
matchError (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs StructType
t1' StructType
t2'
link :: Bool -> VName -> Int -> StructType -> m ()
link Bool
ord' =
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifySizes m
linkDims Usage
usage [VName]
bound BreadCrumbs
bcs
where
linkDims :: UnifySizes m
linkDims
| Bool
ord' = UnifySizes m -> UnifySizes m
forall (m :: * -> *). UnifySizes m -> UnifySizes m
flipUnifySizes UnifySizes m
onDims
| Bool
otherwise = UnifySizes m
onDims
unifyTypeArg :: BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Exp
d1) (TypeArgDim Exp
d2) =
BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs' (Bool -> Exp -> Exp -> (Exp, Exp)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Exp
d1 Exp
d2)
unifyTypeArg BreadCrumbs
bcs' (TypeArgType StructType
t) (TypeArgType StructType
arg_t) =
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
t StructType
arg_t
unifyTypeArg BreadCrumbs
bcs' TypeArg Exp
_ TypeArg Exp
_ =
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
Usage
usage
Notes
forall a. Monoid a => a
mempty
BreadCrumbs
bcs'
Doc ()
"Cannot unify a type argument with a dimension argument (or vice versa)."
onDims' :: BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs' (Exp
d1, Exp
d2) =
UnifySizes m
onDims
BreadCrumbs
bcs'
[VName]
bound
VName -> Maybe Int
nonrigid
(TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d1)
(TypeSubs -> Exp -> Exp
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Exp
d2)
case (StructType
t1', StructType
t2') of
(Scalar (Prim PrimType
pt1), Scalar (Prim PrimType
pt2))
| PrimType
pt1 PrimType -> PrimType -> Bool
forall a. Eq a => a -> a -> Bool
== PrimType
pt2 -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
( Scalar (Record Map Name StructType
fs),
Scalar (Record Map Name StructType
arg_fs)
)
| Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs ->
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
fs Map Name StructType
arg_fs
| Bool
otherwise -> do
let missing :: [Name]
missing =
(Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs) (Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fs)
[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fs) (Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
arg_fs)
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Unshared fields:" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((Name -> Doc ()) -> [Name] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty [Name]
missing) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
( Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Exp]
targs),
Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Exp]
arg_targs)
)
| VName
tn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
[TypeArg Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
targs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Exp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Exp]
arg_targs -> do
let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc () -> BreadCrumb
Matching Doc ()
"When matching type arguments.") BreadCrumbs
bcs
(TypeArg Exp -> TypeArg Exp -> m ())
-> [TypeArg Exp] -> [TypeArg Exp] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Exp]
targs [TypeArg Exp]
arg_targs
( Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v1) []),
Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v2) [])
) ->
case (VName -> Maybe Int
nonrigid VName
v1, VName -> Maybe Int
nonrigid VName
v2) of
(Maybe Int
Nothing, Maybe Int
Nothing) -> m ()
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lvl2 -> Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl1 StructType
t2'
| Bool
otherwise -> Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl2 StructType
t1'
(Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v1) []), StructType
_)
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v1 ->
Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl StructType
t2'
(StructType
_, Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v2) []))
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v2 ->
Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl StructType
t1'
( Scalar (Arrow NoUniqueness
_ PName
p1 Diet
d1 StructType
a1 (RetType [VName]
b1_dims TypeBase Exp Uniqueness
b1)),
Scalar (Arrow NoUniqueness
_ PName
p2 Diet
d2 StructType
a2 (RetType [VName]
b2_dims TypeBase Exp Uniqueness
b2))
)
| (Diet -> Diet -> Bool) -> (Diet, Diet) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Diet -> Diet -> Bool
forall a. Ord a => a -> a -> Bool
(<) ((Diet, Diet) -> Bool) -> (Diet, Diet) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Diet -> Diet -> (Diet, Diet)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Diet
d1 Diet
d2 -> do
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-consuming-param" (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Parameters"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d1 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
a1)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"and"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d2 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
a2)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"are incompatible regarding consuming their arguments."
| (Uniqueness -> Uniqueness -> Bool)
-> (Uniqueness, Uniqueness) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Uniqueness -> Uniqueness -> Bool
forall a. Ord a => a -> a -> Bool
(<) ((Uniqueness, Uniqueness) -> Bool)
-> (Uniqueness, Uniqueness) -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Uniqueness -> Uniqueness -> (Uniqueness, Uniqueness)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord (TypeBase Exp Uniqueness -> Uniqueness
forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness TypeBase Exp Uniqueness
b2) (TypeBase Exp Uniqueness -> Uniqueness
forall shape. TypeBase shape Uniqueness -> Uniqueness
uniqueness TypeBase Exp Uniqueness
b1) -> do
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-return-uniqueness" (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Return types"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d1 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> TypeBase Exp Uniqueness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase Exp Uniqueness -> Doc ann
pretty TypeBase Exp Uniqueness
b1)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"and"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Diet -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Diet -> Doc ann
pretty Diet
d2 Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> TypeBase Exp Uniqueness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase Exp Uniqueness -> Doc ann
pretty TypeBase Exp Uniqueness
b2)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"have incompatible uniqueness."
| Bool
otherwise -> do
let (Constraint
r1, Constraint
r2) =
Bool -> Constraint -> Constraint -> (Constraint, Constraint)
forall {a}. Bool -> a -> a -> (a, a)
swap
Bool
ord
(Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing Loc
forall a. Monoid a => a
mempty)
(Loc -> RigidSource -> Constraint
UnknownSize Loc
forall a. Monoid a => a
mempty RigidSource
RigidUnify)
Int
lvl <- m Int
forall (m :: * -> *). MonadUnify m => m Int
curLevel
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ([(VName, (Int, Constraint))] -> Constraints
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((VName -> (VName, (Int, Constraint)))
-> [VName] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> [a] -> [b]
map (,(Int
lvl, Constraint
r1)) [VName]
b1_dims) <>)
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ([(VName, (Int, Constraint))] -> Constraints
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((VName -> (VName, (Int, Constraint)))
-> [VName] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> [a] -> [b]
map (,(Int
lvl, Constraint
r2)) [VName]
b2_dims) <>)
let bound' :: [VName]
bound' = [VName]
bound [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> (PName -> Maybe VName) -> [PName] -> [VName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PName -> Maybe VName
pname [PName
p1, PName
p2] [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b1_dims [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims
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)
(TypeBase Exp Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Exp Uniqueness
b1')
(TypeBase Exp Uniqueness -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct TypeBase Exp Uniqueness
b2')
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ \Constraints
m -> (Constraints -> VName -> Constraints)
-> Constraints -> [VName] -> Constraints
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((VName -> Constraints -> Constraints)
-> Constraints -> VName -> Constraints
forall a b c. (a -> b -> c) -> b -> a -> c
flip VName -> Constraints -> Constraints
forall k a. Ord k => k -> Map k a -> Map k a
M.delete) Constraints
m ([VName]
b1_dims [VName] -> [VName] -> [VName]
forall a. Semigroup a => a -> a -> a
<> [VName]
b2_dims)
where
(TypeBase Exp Uniqueness
b1', TypeBase Exp Uniqueness
b2') =
case (PName
p1, PName
p2) of
(Named VName
p1', Named VName
p2') ->
let f :: VName -> Maybe (Subst t)
f VName
v
| VName
v VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
p2' = Subst t -> Maybe (Subst t)
forall a. a -> Maybe a
Just (Subst t -> Maybe (Subst t)) -> Subst t -> Maybe (Subst t)
forall a b. (a -> b) -> a -> b
$ Exp -> Subst t
forall t. Exp -> Subst t
ExpSubst (Exp -> Subst t) -> Exp -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
p1') SrcLoc
forall a. Monoid a => a
mempty
| Bool
otherwise = Maybe (Subst t)
forall a. Maybe a
Nothing
in (TypeBase Exp Uniqueness
b1, TypeSubs -> TypeBase Exp Uniqueness -> TypeBase Exp Uniqueness
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
f TypeBase Exp Uniqueness
b2)
(PName
_, PName
_) ->
(TypeBase Exp Uniqueness
b1, TypeBase Exp Uniqueness
b2)
pname :: PName -> Maybe VName
pname (Named VName
x) = VName -> Maybe VName
forall a. a -> Maybe a
Just VName
x
pname PName
Unnamed = Maybe VName
forall a. Maybe a
Nothing
(Array {}, Array {})
| Shape (Exp
t1_d : [Exp]
_) <- StructType -> Shape Exp
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t1',
Shape (Exp
t2_d : [Exp]
_) <- StructType -> Shape Exp
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t2',
Just StructType
t1'' <- Int -> StructType -> Maybe StructType
forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
peelArray Int
1 StructType
t1',
Just StructType
t2'' <- Int -> StructType -> Maybe StructType
forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
peelArray Int
1 StructType
t2' -> do
BreadCrumbs -> (Exp, Exp) -> m ()
onDims' BreadCrumbs
bcs (Bool -> Exp -> Exp -> (Exp, Exp)
forall {a}. Bool -> a -> a -> (a, a)
swap Bool
ord Exp
t1_d Exp
t2_d)
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs StructType
t1'' StructType
t2''
( Scalar (Sum Map Name [StructType]
cs),
Scalar (Sum Map Name [StructType]
arg_cs)
)
| Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs ->
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs Map Name [StructType]
arg_cs
| Bool
otherwise ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> Map Name [StructType] -> Doc ()
forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name [StructType]
arg_cs Map Name [StructType]
cs
(StructType, StructType)
_ -> m ()
forall {a}. m a
failure
anyBound :: [VName] -> ExpBase Info VName -> Bool
anyBound :: [VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e = (VName -> Bool) -> [VName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (Exp -> FV
freeInExp Exp
e)) [VName]
bound
unifySizes :: (MonadUnify m) => Usage -> UnifySizes m
unifySizes :: forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
e1 Exp
e2
| Just [(Exp, Exp)]
es <- Exp -> Exp -> Maybe [(Exp, Exp)]
similarExps Exp
e1 Exp
e2 =
((Exp, Exp) -> m ()) -> [(Exp, Exp)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ())
-> (Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
forall a b. (a -> b) -> a -> b
$ Usage -> UnifySizes m
forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid) [(Exp, Exp)]
es
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid (Var QualName VName
v1 Info StructType
_ SrcLoc
_) Exp
e2
| Just Int
lvl1 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1),
Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e2) Bool -> Bool -> Bool
|| (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1 VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v1) Int
lvl1 Exp
e2
unifySizes Usage
usage BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Exp
e1 (Var QualName VName
v2 Info StructType
_ SrcLoc
_)
| Just Int
lvl2 <- VName -> Maybe Int
nonrigid (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2),
Bool -> Bool
not ([VName] -> Exp -> Bool
anyBound [VName]
bound Exp
e1) Bool -> Bool -> Bool
|| (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2 VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) =
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
v2) Int
lvl2 Exp
e1
unifySizes Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Exp
e1 Exp
e2 = do
Notes
notes <- Notes -> Notes -> Notes
forall a. Semigroup a => a -> a -> a
(<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e2 m (Notes -> Notes) -> m Notes -> m Notes
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e2
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Sizes"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e1)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"and"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e2)
Doc () -> Doc () -> Doc ()
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 = UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith (Usage -> UnifySizes m
forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage) Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
occursCheck ::
(MonadUnify m) =>
Usage ->
BreadCrumbs ->
VName ->
StructType ->
m ()
occursCheck :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp =
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VName
vn VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` StructType -> Set VName
forall dim as. TypeBase dim as -> Set VName
typeVars StructType
tp) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Occurs check: cannot instantiate"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
tp
Doc () -> Doc () -> Doc ()
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 <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
Constraints -> StructType -> m ()
forall {m :: * -> *} {u}.
MonadUnify m =>
Constraints -> TypeBase Exp u -> m ()
checkType Constraints
constraints StructType
tp
where
checkType :: Constraints -> TypeBase Exp u -> m ()
checkType Constraints
constraints TypeBase Exp u
t =
(VName -> m ()) -> Set VName -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Constraints -> VName -> m ()
forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
check Constraints
constraints) (Set VName -> m ()) -> Set VName -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase Exp u -> Set VName
forall dim as. TypeBase dim as -> Set VName
typeVars TypeBase Exp u
t Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> FV -> Set VName
fvVars (TypeBase Exp u -> FV
forall u. TypeBase Exp u -> FV
freeInType TypeBase Exp u
t)
check :: Constraints -> VName -> m ()
check Constraints
constraints VName
v
| Just (Int
lvl, Constraint
c) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints,
Int
lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
max_lvl =
if Constraint -> Bool
rigidConstraint Constraint
c
then VName -> m ()
forall {m :: * -> *} {v} {b}. (MonadUnify m, IsName v) => v -> m b
scopeViolation VName
v
else (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
max_lvl, Constraint
c)
| Bool
otherwise =
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
scopeViolation :: v -> m b
scopeViolation v
v = do
Notes
notes <- Usage -> StructType -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> StructType -> m Notes
typeNotes Usage
usage StructType
tp
Usage -> Notes -> BreadCrumbs -> Doc () -> m b
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc () -> m b) -> Doc () -> m b
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
tp)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"with"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"(scope violation)."
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"This is because"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (v -> Doc ()
forall a. v -> Doc a
forall v a. IsName v => v -> Doc a
prettyName v
v)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is rigidly bound in a deeper scope."
linkVarToType ::
(MonadUnify m) =>
UnifySizes m ->
Usage ->
[VName] ->
BreadCrumbs ->
VName ->
Level ->
StructType ->
m ()
linkVarToType :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs VName
vn Int
lvl StructType
tp_unnorm = do
StructType
tp <- StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
tp_unnorm
Usage -> BreadCrumbs -> VName -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> StructType -> m ()
occursCheck Usage
usage BreadCrumbs
bcs VName
vn StructType
tp
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
vn Int
lvl StructType
tp
Constraints
constraints <- m 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 VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
witnessed Bool -> Bool -> Bool
|| VName
v VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
not_witnessed
ext :: [VName]
ext = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
used [VName]
bound
case (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Set VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set VName
witnessed) [VName]
ext of
[] ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint ([VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp) Usage
usage)
[VName]
problems ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
withIndexLink Doc ()
"unify-param-existential" (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Parameter(s) "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((VName -> Doc ()) -> [VName] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Doc () -> Doc ()) -> (VName -> Doc ()) -> VName -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName) [VName]
problems)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" used as size(s) would go out of scope."
let unliftedBcs :: a -> BreadCrumbs
unliftedBcs a
unlifted_usage =
BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
( Doc () -> BreadCrumb
Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
forall a b. (a -> b) -> a -> b
$
Doc ()
"When verifying that"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
"is not instantiated with a function type, due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc ()
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
unlifted_usage
)
BreadCrumbs
bcs
case (Int, Constraint) -> Constraint
forall a b. (a, b) -> b
snd ((Int, Constraint) -> Constraint)
-> Maybe (Int, Constraint) -> Maybe Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (NoConstraint Liftedness
Unlifted Usage
unlift_usage) -> do
m ()
link
Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (Usage -> BreadCrumbs
forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
unlift_usage) StructType
tp
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((VName -> Bool) -> Set VName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (VName -> [VName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) (FV -> Set VName
fvVars (StructType -> FV
forall u. TypeBase Exp u -> FV
freeInType StructType
tp))) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type variable"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"cannot be instantiated with type containing anonymous sizes:"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
tp)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Text -> Doc ()
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
Usage -> StructType -> m ()
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> TypeBase dim u -> m ()
equalityType Usage
usage StructType
tp
Just (Overloaded [PrimType]
ts Usage
old_usage)
| StructType
tp StructType -> [StructType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (PrimType -> StructType) -> [PrimType] -> [StructType]
forall a b. (a -> b) -> [a] -> [b]
map (ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
-> (PrimType -> ScalarTypeBase Exp NoUniqueness)
-> PrimType
-> StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimType -> ScalarTypeBase Exp NoUniqueness
forall dim u. PrimType -> ScalarTypeBase dim u
Prim) [PrimType]
ts -> do
m ()
link
case StructType
tp of
Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) [])
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints ->
Usage -> VName -> [PrimType] -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
StructType
_ ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot instantiate"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
tp)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be one of"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
old_usage
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (HasFields Liftedness
l Map Name StructType
required_fields Usage
old_usage) -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
== Liftedness
Unlifted) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (Usage -> BreadCrumbs
forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
old_usage) StructType
tp
case StructType
tp of
Scalar (Record Map Name StructType
tp_fields)
| (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name -> Map Name StructType -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map Name StructType
tp_fields) ([Name] -> Bool) -> [Name] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
required_fields -> do
Map Name StructType
required_fields' <- (StructType -> m StructType)
-> Map Name StructType -> m (Map Name StructType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Name a -> m (Map Name b)
mapM StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully Map Name StructType
required_fields
let tp' :: StructType
tp' = ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
-> ScalarTypeBase Exp NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name StructType -> ScalarTypeBase Exp NoUniqueness
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record (Map Name StructType -> ScalarTypeBase Exp NoUniqueness)
-> Map Name StructType -> ScalarTypeBase Exp NoUniqueness
forall a b. (a -> b) -> a -> b
$ Map Name StructType
required_fields Map Name StructType -> Map Name StructType -> Map Name StructType
forall a. Semigroup a => a -> a -> a
<> Map Name StructType
tp_fields
ext :: [VName]
ext = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (StructType -> FV
forall u. TypeBase Exp u -> FV
freeInType StructType
tp')) [VName]
bound
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint ([VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp') Usage
usage)
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
required_fields' Map Name StructType
tp_fields
Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) []) -> do
case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
Just (Int
_, HasFields Liftedness
_ Map Name StructType
tp_fields Usage
_) ->
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
required_fields Map Name StructType
tp_fields
Just (Int
_, NoConstraint {}) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, Equality {}) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe (Int, Constraint)
_ -> do
Notes
notes <- Notes -> Notes -> Notes
forall a. Semigroup a => a -> a -> a
(<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn m (Notes -> Notes) -> m Notes -> m Notes
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v
Notes -> m ()
forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noRecordType Notes
notes
m ()
link
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
((Int, Constraint) -> (Int, Constraint) -> (Int, Constraint))
-> VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith
(Int, Constraint) -> (Int, Constraint) -> (Int, Constraint)
forall {a}.
(Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineFields
VName
v
(Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
l Map Name StructType
required_fields Usage
old_usage)
where
combineFields :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineFields (Int
_, HasFields Liftedness
l1 Map Name StructType
fs1 Usage
usage1) (a
_, HasFields Liftedness
l2 Map Name StructType
fs2 Usage
_) =
(Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields (Liftedness
l1 Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
`min` Liftedness
l2) (Map Name StructType -> Map Name StructType -> Map Name StructType
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Name StructType
fs1 Map Name StructType
fs2) Usage
usage1)
combineFields (Int, Constraint)
hasfs (a, Constraint)
_ = (Int, Constraint)
hasfs
StructType
_ ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot instantiate"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
tp)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"as"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"must be a record with fields"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (ScalarTypeBase Exp NoUniqueness -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. ScalarTypeBase Exp NoUniqueness -> Doc ann
pretty (Map Name StructType -> ScalarTypeBase Exp NoUniqueness
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record Map Name StructType
required_fields))
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
old_usage
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (HasConstrs Liftedness
l Map Name [StructType]
required_cs Usage
old_usage) -> do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Liftedness
l Liftedness -> Liftedness -> Bool
forall a. Eq a => a -> a -> Bool
== Liftedness
Unlifted) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (Usage -> BreadCrumbs
forall {a}. Pretty a => a -> BreadCrumbs
unliftedBcs Usage
old_usage) StructType
tp
case StructType
tp of
Scalar (Sum Map Name [StructType]
ts)
| (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name -> Map Name [StructType] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map Name [StructType]
ts) ([Name] -> Bool) -> [Name] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
required_cs -> do
let tp' :: StructType
tp' = ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
-> ScalarTypeBase Exp NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum (Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness)
-> Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
forall a b. (a -> b) -> a -> b
$ Map Name [StructType]
required_cs Map Name [StructType]
-> Map Name [StructType] -> Map Name [StructType]
forall a. Semigroup a => a -> a -> a
<> Map Name [StructType]
ts
ext :: [VName]
ext = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` FV -> Set VName
fvVars (StructType -> FV
forall u. TypeBase Exp u -> FV
freeInType StructType
tp')) [VName]
bound
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, StructRetType -> Usage -> Constraint
Constraint ([VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext StructType
tp') Usage
usage)
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
ts
| Bool
otherwise ->
Map Name [StructType] -> Map Name [StructType] -> Notes -> m ()
forall {m :: * -> *} {t} {a}.
MonadUnify m =>
Map Name t -> Map Name t -> Notes -> m a
unsharedConstructors Map Name [StructType]
required_cs Map Name [StructType]
ts (Notes -> m ()) -> m Notes -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn
Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) []) -> do
case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Constraints
constraints of
Just (Int
_, HasConstrs Liftedness
_ Map Name [StructType]
v_cs Usage
_) ->
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
v_cs
Just (Int
_, NoConstraint {}) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, Equality {}) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe (Int, Constraint)
_ -> do
Notes
notes <- Notes -> Notes -> Notes
forall a. Semigroup a => a -> a -> a
(<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn m (Notes -> Notes) -> m Notes -> m Notes
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
v
Notes -> m ()
forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noSumType Notes
notes
m ()
link
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
((Int, Constraint) -> (Int, Constraint) -> (Int, Constraint))
-> VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith
(Int, Constraint) -> (Int, Constraint) -> (Int, Constraint)
forall {a}.
(Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs
VName
v
(Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l Map Name [StructType]
required_cs Usage
old_usage)
where
combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs (Int
_, HasConstrs Liftedness
l1 Map Name [StructType]
cs1 Usage
usage1) (a
_, HasConstrs Liftedness
l2 Map Name [StructType]
cs2 Usage
_) =
(Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs (Liftedness
l1 Liftedness -> Liftedness -> Liftedness
forall a. Ord a => a -> a -> a
`min` Liftedness
l2) (Map Name [StructType]
-> Map Name [StructType] -> Map Name [StructType]
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
_ -> Notes -> m ()
forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
noSumType (Notes -> m ()) -> m Notes -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VName -> m Notes
forall (m :: * -> *). MonadUnify m => VName -> m Notes
typeVarNotes VName
vn
Maybe Constraint
_ -> m ()
link
where
unsharedConstructors :: Map Name t -> Map Name t -> Notes -> m a
unsharedConstructors Map Name t
cs1 Map Name t
cs2 Notes
notes =
Usage -> Notes -> BreadCrumbs -> Doc () -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
Usage
usage
Notes
notes
BreadCrumbs
bcs
(Map Name t -> Map Name t -> Doc ()
forall t a. Map Name t -> Map Name t -> Doc a
unsharedConstructorsMsg Map Name t
cs1 Map Name t
cs2)
noSumType :: Notes -> m a
noSumType Notes
notes =
Usage -> Notes -> BreadCrumbs -> Doc () -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
Usage
usage
Notes
notes
BreadCrumbs
bcs
Doc ()
"Cannot unify a sum type with a non-sum type."
noRecordType :: Notes -> m a
noRecordType Notes
notes =
Usage -> Notes -> BreadCrumbs -> Doc () -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError
Usage
usage
Notes
notes
BreadCrumbs
bcs
Doc ()
"Cannot unify a record type with a non-record type."
linkVarToDim ::
(MonadUnify m) =>
Usage ->
BreadCrumbs ->
VName ->
Level ->
Exp ->
m ()
linkVarToDim :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
vn Int
lvl Exp
e = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
(VName -> m ()) -> Set VName -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Constraints -> VName -> m ()
forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
checkVar Constraints
constraints) (Set VName -> m ()) -> Set VName -> m ()
forall a b. (a -> b) -> a -> b
$ FV -> Set VName
fvVars (FV -> Set VName) -> FV -> Set VName
forall a b. (a -> b) -> a -> b
$ Exp -> FV
freeInExp Exp
e
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Maybe Exp -> Usage -> Constraint
Size (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
e) Usage
usage)
where
checkVar :: Constraints -> VName -> m ()
checkVar Constraints
_ VName
dim'
| VName
vn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
dim' = do
Notes
notes <- Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Occurs check: cannot instantiate"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
checkVar Constraints
constraints VName
dim'
| Just (Int
dim_lvl, Constraint
c) <- VName
dim' VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Constraints
constraints,
Int
dim_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lvl =
case Constraint
c of
ParamSize {} -> do
Notes
notes <- Usage -> Exp -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Exp -> m Notes
dimNotes Usage
usage Exp
e
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot link size"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Exp -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"(scope violation)."
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"This is because"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (QualName VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. QualName VName -> Doc ann
pretty (QualName VName -> Doc ()) -> QualName VName -> Doc ()
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
dim')
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is not in scope when"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is introduced."
Constraint
_ -> (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim' (Int
lvl, Constraint
c)
checkVar Constraints
_ VName
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
mustBeOneOf :: (MonadUnify m) => [PrimType] -> Usage -> StructType -> m ()
mustBeOneOf :: forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType
req_t] Usage
usage StructType
t = Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (PrimType -> ScalarTypeBase Exp NoUniqueness
forall dim u. PrimType -> ScalarTypeBase dim u
Prim PrimType
req_t)) StructType
t
mustBeOneOf [PrimType]
ts Usage
usage StructType
t = do
StructType
t' <- StructType -> m StructType
forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
let isRigid' :: VName -> Bool
isRigid' VName
v = VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints
case StructType
t' of
Scalar (TypeVar NoUniqueness
_ (QualName [] VName
v) [])
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ VName -> Bool
isRigid' VName
v -> Usage -> VName -> [PrimType] -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> VName -> [PrimType] -> m ()
linkVarToTypes Usage
usage VName
v [PrimType]
ts
Scalar (Prim PrimType
pt) | PrimType
pt PrimType -> [PrimType] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ts -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
StructType
_ -> m ()
forall {a}. m a
failure
where
failure :: m a
failure =
Usage -> Notes -> BreadCrumbs -> Doc () -> m a
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m a) -> Doc () -> m a
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"with any of "
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
Doc () -> Doc () -> Doc ()
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 <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn (Constraints -> Maybe (Int, Constraint))
-> m Constraints -> m (Maybe (Int, Constraint))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case Maybe (Int, Constraint)
vn_constraint of
Just (Int
lvl, Overloaded [PrimType]
vn_ts Usage
vn_usage) ->
case [PrimType]
ts [PrimType] -> [PrimType] -> [PrimType]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [PrimType]
vn_ts of
[] ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"but also one of"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
vn_ts)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
vn_usage
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
[PrimType]
ts' -> (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts' Usage
usage)
Just (Int
_, HasConstrs Liftedness
_ Map Name [StructType]
_ Usage
vn_usage) ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be sum type due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
vn_usage
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (Int
_, HasFields Liftedness
_ Map Name StructType
_ Usage
vn_usage) ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type constrained to one of"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
", but also inferred to be record due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
vn_usage
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Just (Int
lvl, Constraint
_) -> (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, [PrimType] -> Usage -> Constraint
Overloaded [PrimType]
ts Usage
usage)
Maybe (Int, Constraint)
Nothing ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot constrain type to one of" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> [Doc ()] -> Doc ()
forall a. [Doc a] -> Doc a
commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PrimType -> Doc ann
pretty [PrimType]
ts)
equalityType ::
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage ->
TypeBase dim u ->
m ()
equalityType :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> TypeBase dim u -> m ()
equalityType Usage
usage TypeBase dim u
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim u -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim u
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type " Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeBase dim u -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase dim u -> Doc ann
pretty TypeBase dim u
t) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality (may contain function)."
(VName -> m ()) -> Set VName -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> m ()
forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeEquality (Set VName -> m ()) -> Set VName -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim u -> Set VName
forall dim as. TypeBase dim as -> Set VName
typeVars TypeBase dim u
t
where
mustBeEquality :: VName -> m ()
mustBeEquality VName
vn = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (Int
_, Constraint (RetType [] (Scalar (TypeVar NoUniqueness
_ (QualName [] VName
vn') []))) Usage
_) ->
VName -> m ()
mustBeEquality VName
vn'
Just (Int
_, Constraint (RetType [VName]
_ StructType
vn_t) Usage
cusage)
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ StructType -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero StructType
vn_t ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (TypeBase dim u -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase dim u -> Doc ann
pretty TypeBase dim u
t)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"Constrained to be higher-order due to"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Usage -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Usage -> Doc ann
pretty Usage
cusage
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
| Bool
otherwise -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
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
_) ->
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, Equality {}) ->
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe (Int, Constraint)
_ ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"does not support equality."
zeroOrderTypeWith ::
(MonadUnify m) =>
Usage ->
BreadCrumbs ->
StructType ->
m ()
zeroOrderTypeWith :: forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> StructType -> m ()
zeroOrderTypeWith Usage
usage BreadCrumbs
bcs StructType
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (StructType -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero StructType
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
(VName -> m ()) -> [VName] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> m ()
forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder ([VName] -> m ()) -> (StructType -> [VName]) -> StructType -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName])
-> (StructType -> Set VName) -> StructType -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StructType -> Set VName
forall dim as. TypeBase dim as -> Set VName
typeVars (StructType -> m ()) -> m StructType -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StructType -> m StructType
forall (m :: * -> *). MonadUnify m => StructType -> m StructType
normType StructType
t
where
mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Unlifted Usage
usage)
Just (Int
lvl, HasFields Liftedness
_ Map Name StructType
fs Usage
_) ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
Unlifted Map Name StructType
fs Usage
usage)
Just (Int
lvl, HasConstrs Liftedness
_ Map Name [StructType]
cs Usage
_) ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
vn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
Unlifted Map Name [StructType]
cs Usage
usage)
Just (Int
_, ParamType Liftedness
Lifted Loc
ploc) ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type parameter"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> String
forall a. Located a => a -> String
locStr Loc
ploc)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"may be a function."
Maybe (Int, Constraint)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
zeroOrderType ::
(MonadUnify m) => Usage -> T.Text -> StructType -> m ()
zeroOrderType :: forall (m :: * -> *).
MonadUnify m =>
Usage -> Text -> StructType -> m ()
zeroOrderType Usage
usage Text
desc =
Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> StructType -> m ()
zeroOrderTypeWith Usage
usage (BreadCrumbs -> StructType -> m ())
-> BreadCrumbs -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb BreadCrumb
bc BreadCrumbs
noBreadCrumbs
where
bc :: BreadCrumb
bc = Doc () -> BreadCrumb
Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
forall a b. (a -> b) -> a -> b
$ Doc ()
"When checking" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
desc
arrayElemTypeWith ::
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage ->
BreadCrumbs ->
TypeBase dim u ->
m ()
arrayElemTypeWith :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim u
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim u -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim u
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (TypeBase dim u -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase dim u -> Doc ann
pretty TypeBase dim u
t) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
</> Doc ()
"found to be functional."
(VName -> m ()) -> [VName] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VName -> m ()
forall {m :: * -> *}. MonadUnify m => VName -> m ()
mustBeZeroOrder ([VName] -> m ())
-> (TypeBase dim u -> [VName]) -> TypeBase dim u -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName])
-> (TypeBase dim u -> Set VName) -> TypeBase dim u -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim u -> Set VName
forall dim as. TypeBase dim as -> Set VName
typeVars (TypeBase dim u -> m ()) -> TypeBase dim u -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim u
t
where
mustBeZeroOrder :: VName -> m ()
mustBeZeroOrder VName
vn = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
vn Constraints
constraints of
Just (Int
lvl, NoConstraint Liftedness
_ Usage
_) ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
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 Loc
ploc)
| Liftedness
l Liftedness -> [Liftedness] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Liftedness
Lifted, Liftedness
SizeLifted] ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Type parameter"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName VName
vn)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"bound at"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc ()
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Loc -> String
forall a. Located a => a -> String
locStr Loc
ploc)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"is lifted and cannot be an array element."
Maybe (Int, Constraint)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
arrayElemType ::
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage ->
T.Text ->
TypeBase dim u ->
m ()
arrayElemType :: forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> Text -> TypeBase dim u -> m ()
arrayElemType Usage
usage Text
desc =
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
forall (m :: * -> *) dim u.
(MonadUnify m, Pretty (Shape dim), Pretty u) =>
Usage -> BreadCrumbs -> TypeBase dim u -> m ()
arrayElemTypeWith Usage
usage (BreadCrumbs -> TypeBase dim u -> m ())
-> BreadCrumbs -> TypeBase dim u -> m ()
forall a b. (a -> b) -> a -> b
$ BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb BreadCrumb
bc BreadCrumbs
noBreadCrumbs
where
bc :: BreadCrumb
bc = Doc () -> BreadCrumb
Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
forall a b. (a -> b) -> a -> b
$ Doc ()
"When checking" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Text -> Doc ()
forall a. Text -> Doc a
textwrap Text
desc
unifySharedFields ::
(MonadUnify m) =>
UnifySizes m ->
Usage ->
[VName] ->
BreadCrumbs ->
M.Map Name StructType ->
M.Map Name StructType ->
m ()
unifySharedFields :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name StructType
-> Map Name StructType
-> m ()
unifySharedFields UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name StructType
fs1 Map Name StructType
fs2 =
[(Name, (StructType, StructType))]
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name (StructType, StructType)
-> [(Name, (StructType, StructType))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name (StructType, StructType)
-> [(Name, (StructType, StructType))])
-> Map Name (StructType, StructType)
-> [(Name, (StructType, StructType))]
forall a b. (a -> b) -> a -> b
$ (StructType -> StructType -> (StructType, StructType))
-> Map Name StructType
-> Map Name StructType
-> Map Name (StructType, StructType)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name StructType
fs1 Map Name StructType
fs2) (((Name, (StructType, StructType)) -> m ()) -> m ())
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Name
f, (StructType
t1, StructType
t2)) ->
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound (BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
f]) BreadCrumbs
bcs) StructType
t1 StructType
t2
unifySharedConstructors ::
(MonadUnify m) =>
UnifySizes m ->
Usage ->
[VName] ->
BreadCrumbs ->
M.Map Name [StructType] ->
M.Map Name [StructType] ->
m ()
unifySharedConstructors :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs1 Map Name [StructType]
cs2 =
[(Name, ([StructType], [StructType]))]
-> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Name ([StructType], [StructType])
-> [(Name, ([StructType], [StructType]))]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name ([StructType], [StructType])
-> [(Name, ([StructType], [StructType]))])
-> Map Name ([StructType], [StructType])
-> [(Name, ([StructType], [StructType]))]
forall a b. (a -> b) -> a -> b
$ ([StructType] -> [StructType] -> ([StructType], [StructType]))
-> Map Name [StructType]
-> Map Name [StructType]
-> Map Name ([StructType], [StructType])
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [StructType]
cs1 Map Name [StructType]
cs2) (((Name, ([StructType], [StructType])) -> m ()) -> m ())
-> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
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
| [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> Int
forall a. [a] -> Int
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
(StructType -> StructType -> m ())
-> [StructType] -> [StructType] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') [StructType]
f1 [StructType]
f2
| Bool
otherwise =
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot unify constructor" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall ann. Name -> Doc ann
forall v a. IsName v => v -> Doc a
prettyName Name
c) Doc () -> Doc () -> Doc ()
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 <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case StructType
t of
Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [])
| Just (Int
lvl, NoConstraint Liftedness
l Usage
_) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
(StructType -> m ()) -> [StructType] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
noBreadCrumbs VName
tn Int
lvl) [StructType]
fs
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l (Name -> [StructType] -> Map Name [StructType]
forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs) Usage
usage)
| Just (Int
lvl, HasConstrs Liftedness
l Map Name [StructType]
cs Usage
_) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints ->
case Name -> Map Name [StructType] -> Maybe [StructType]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
c Map Name [StructType]
cs of
Maybe [StructType]
Nothing ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
HasConstrs Liftedness
l (Name
-> [StructType] -> Map Name [StructType] -> Map Name [StructType]
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'
| [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs' -> (StructType -> StructType -> m ())
-> [StructType] -> [StructType] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage) [StructType]
fs [StructType]
fs'
| Bool
otherwise ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Different arity for constructor" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
c) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
Scalar (Sum Map Name [StructType]
cs) ->
case Name -> Map Name [StructType] -> Maybe [StructType]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
c Map Name [StructType]
cs of
Maybe [StructType]
Nothing ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Constuctor" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
c) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"not present in type."
Just [StructType]
fs'
| [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs' -> (StructType -> StructType -> m ())
-> [StructType] -> [StructType] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage) [StructType]
fs [StructType]
fs'
| Bool
otherwise ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
forall a b. (a -> b) -> a -> b
$
Doc ()
"Different arity for constructor" Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
c) Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"."
StructType
_ ->
Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
-> ScalarTypeBase Exp NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum (Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness)
-> Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
forall a b. (a -> b) -> a -> b
$ Name -> [StructType] -> Map Name [StructType]
forall k a. k -> a -> Map k a
M.singleton Name
c [StructType]
fs
mustHaveFieldWith ::
(MonadUnify m) =>
UnifySizes m ->
Usage ->
[VName] ->
BreadCrumbs ->
Name ->
StructType ->
m StructType
mustHaveFieldWith :: forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Name
-> StructType
-> m StructType
mustHaveFieldWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l StructType
t = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
StructType
l_type <- Loc -> Name -> m StructType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> m (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> Name -> m (TypeBase dim als)
newTypeVar (Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage) Name
"t"
case StructType
t of
Scalar (TypeVar NoUniqueness
_ (QualName [VName]
_ VName
tn) [])
| Just (Int
lvl, NoConstraint {}) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
scopeCheck Usage
usage BreadCrumbs
bcs VName
tn Int
lvl StructType
l_type
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
tn (Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
Lifted (Name -> StructType -> Map Name StructType
forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type) Usage
usage)
StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type
| Just (Int
lvl, HasFields Liftedness
lifted Map Name StructType
fields Usage
_) <- VName -> Constraints -> Maybe (Int, Constraint)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
tn Constraints
constraints -> do
case Name -> Map Name StructType -> Maybe StructType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name StructType
fields of
Just StructType
t' -> UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs StructType
l_type StructType
t'
Maybe StructType
Nothing ->
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> m ())
-> (Constraints -> Constraints) -> m ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert
VName
tn
(Int
lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
HasFields Liftedness
lifted (Name -> StructType -> Map Name StructType -> Map Name StructType
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)
StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type
Scalar (Record Map Name StructType
fields)
| Just StructType
t' <- Name -> Map Name StructType -> Maybe StructType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name StructType
fields -> do
Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
l_type StructType
t'
StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t'
| Bool
otherwise ->
Usage -> Notes -> BreadCrumbs -> Doc () -> m StructType
forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc () -> m a
unifyError Usage
usage Notes
forall a. Monoid a => a
mempty BreadCrumbs
bcs (Doc () -> m StructType) -> Doc () -> m StructType
forall a b. (a -> b) -> a -> b
$
Doc ()
"Attempt to access field"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
l)
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
" of value of type"
Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> TypeBase () () -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeBase () () -> Doc ann
pretty (StructType -> TypeBase () ()
forall dim as. TypeBase dim as -> TypeBase () ()
toStructural StructType
t)
Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
StructType
_ -> do
Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Exp NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
-> ScalarTypeBase Exp NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name StructType -> ScalarTypeBase Exp NoUniqueness
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record (Map Name StructType -> ScalarTypeBase Exp NoUniqueness)
-> Map Name StructType -> ScalarTypeBase Exp NoUniqueness
forall a b. (a -> b) -> a -> b
$ Name -> StructType -> Map Name StructType
forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type
StructType -> m StructType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
l_type
mustHaveField ::
(MonadUnify m) =>
Usage ->
Name ->
StructType ->
m StructType
mustHaveField :: forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> m StructType
mustHaveField Usage
usage = UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Name
-> StructType
-> m StructType
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> Name
-> StructType
-> m StructType
mustHaveFieldWith (Usage -> UnifySizes m
forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
unifySizes Usage
usage) Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
newDimOnMismatch ::
(MonadUnify m) =>
Loc ->
StructType ->
StructType ->
m (StructType, [VName])
newDimOnMismatch :: forall (m :: * -> *).
MonadUnify m =>
Loc -> StructType -> StructType -> m (StructType, [VName])
newDimOnMismatch Loc
loc StructType
t1 StructType
t2 = do
(StructType
t, Map (Exp, Exp) VName
seen) <- StateT (Map (Exp, Exp) VName) m StructType
-> Map (Exp, Exp) VName -> m (StructType, Map (Exp, Exp) VName)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (([VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp)
-> StructType
-> StructType
-> StateT (Map (Exp, Exp) VName) m StructType
forall as (m :: * -> *) d1 d2.
(Monoid as, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
matchDims [VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {p}.
(MonadState (Map (Exp, Exp) VName) (t m), MonadTrans t,
MonadUnify m) =>
p -> Exp -> Exp -> t m Exp
onDims StructType
t1 StructType
t2) Map (Exp, Exp) VName
forall a. Monoid a => a
mempty
(StructType, [VName]) -> m (StructType, [VName])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType
t, Map (Exp, Exp) VName -> [VName]
forall k a. Map k a -> [a]
M.elems Map (Exp, Exp) VName
seen)
where
r :: RigidSource
r = StructType -> StructType -> RigidSource
RigidCond StructType
t1 StructType
t2
same :: (Exp, Exp) -> Bool
same (Exp
e1, Exp
e2) =
Bool -> ([(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (((Exp, Exp) -> Bool) -> [(Exp, Exp)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Exp, Exp) -> Bool
same) (Maybe [(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Maybe [(Exp, Exp)]
similarExps Exp
e1 Exp
e2
onDims :: p -> Exp -> Exp -> t m Exp
onDims p
_ Exp
d1 Exp
d2
| (Exp, Exp) -> Bool
same (Exp
d1, Exp
d2) = Exp -> t m Exp
forall a. a -> t m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
d1
| Bool
otherwise = do
Maybe VName
maybe_d <- (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName))
-> (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
forall a b. (a -> b) -> a -> b
$ (Exp, Exp) -> Map (Exp, Exp) VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Exp
d1, Exp
d2)
case Maybe VName
maybe_d of
Just VName
d -> Exp -> t m Exp
forall a. a -> t m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> t m Exp) -> Exp -> t m Exp
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
d) (SrcLoc -> Exp) -> SrcLoc -> Exp
forall a b. (a -> b) -> a -> b
$ Loc -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Loc
loc
Maybe VName
Nothing -> do
VName
d <- m VName -> t m VName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m VName -> t m VName) -> m VName -> t m VName
forall a b. (a -> b) -> a -> b
$ Loc -> RigidSource -> Name -> m VName
forall a. Located a => a -> RigidSource -> Name -> m VName
forall (m :: * -> *) a.
(MonadUnify m, Located a) =>
a -> RigidSource -> Name -> m VName
newRigidDim Loc
loc RigidSource
r Name
"differ"
(Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ())
-> (Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ()
forall a b. (a -> b) -> a -> b
$ (Exp, Exp) -> VName -> Map (Exp, Exp) VName -> Map (Exp, Exp) VName
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Exp
d1, Exp
d2) VName
d
Exp -> t m Exp
forall a. a -> t m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> t m Exp) -> Exp -> t m Exp
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Exp
sizeFromName (VName -> QualName VName
forall v. v -> QualName v
qualName VName
d) (SrcLoc -> Exp) -> SrcLoc -> Exp
forall a b. (a -> b) -> a -> b
$ Loc -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Loc
loc
unifyMostCommon ::
(MonadUnify m) =>
Usage ->
StructType ->
StructType ->
m (StructType, [VName])
unifyMostCommon :: forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m (StructType, [VName])
unifyMostCommon Usage
usage StructType
t1 StructType
t2 = do
let allOK :: p -> p -> p -> p -> p -> f ()
allOK p
_ p
_ p
_ p
_ p
_ = () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifySizes m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifySizes m
forall {f :: * -> *} {p} {p} {p} {p} {p}.
Applicative f =>
p -> p -> p -> p -> p -> f ()
allOK Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs StructType
t1 StructType
t2
StructType
t1' <- StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t1
StructType
t2' <- StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2
Loc -> StructType -> StructType -> m (StructType, [VName])
forall (m :: * -> *).
MonadUnify m =>
Loc -> StructType -> StructType -> m (StructType, [VName])
newDimOnMismatch (Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage) StructType
t1' StructType
t2'
type UnifyMState = (Constraints, Int)
newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
deriving
( Applicative UnifyM
Applicative UnifyM
-> (forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a. a -> UnifyM a)
-> Monad UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$creturn :: forall a. a -> UnifyM a
return :: forall a. a -> UnifyM a
Monad,
(forall a b. (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b. a -> UnifyM b -> UnifyM a) -> Functor UnifyM
forall a b. a -> UnifyM b -> UnifyM a
forall a b. (a -> b) -> UnifyM a -> UnifyM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
fmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
<$ :: forall a b. a -> UnifyM b -> UnifyM a
Functor,
Functor UnifyM
Functor UnifyM
-> (forall a. a -> UnifyM a)
-> (forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b)
-> (forall a b c.
(a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
-> (forall a b. UnifyM a -> UnifyM b -> UnifyM a)
-> Applicative UnifyM
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> UnifyM a
pure :: forall a. a -> UnifyM a
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
liftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
Applicative,
MonadState UnifyMState,
MonadError TypeError
)
newVar :: Name -> UnifyM VName
newVar :: Name -> UnifyM VName
newVar Name
name = do
(Constraints
x, Int
i) <- UnifyM (Constraints, Int)
forall s (m :: * -> *). MonadState s m => m s
get
(Constraints, Int) -> UnifyM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Constraints
x, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
VName -> UnifyM VName
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName -> UnifyM VName) -> VName -> UnifyM VName
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 = ((Constraints, Int) -> Constraints) -> UnifyM Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Constraints, Int) -> Constraints
forall a b. (a, b) -> a
fst
putConstraints :: Constraints -> UnifyM ()
putConstraints Constraints
x = ((Constraints, Int) -> (Constraints, Int)) -> UnifyM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((Constraints, Int) -> (Constraints, Int)) -> UnifyM ())
-> ((Constraints, Int) -> (Constraints, Int)) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ \(Constraints
_, Int
i) -> (Constraints
x, Int
i)
newTypeVar :: forall als a dim.
(Monoid als, Located a) =>
a -> Name -> UnifyM (TypeBase dim als)
newTypeVar a
loc Name
name = do
VName
v <- Name -> UnifyM VName
newVar Name
name
(Constraints -> Constraints) -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
-> (Constraints -> Constraints) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Int
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
Lifted (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> Loc -> Usage
forall a b. (a -> b) -> a -> b
$ a -> Loc
forall a. Located a => a -> Loc
locOf a
loc)
TypeBase dim als -> UnifyM (TypeBase dim als)
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase dim als -> UnifyM (TypeBase dim als))
-> TypeBase dim als -> UnifyM (TypeBase dim als)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase dim als -> TypeBase dim als
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase dim als -> TypeBase dim als)
-> ScalarTypeBase dim als -> TypeBase dim als
forall a b. (a -> b) -> a -> b
$ als -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim als
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar als
forall a. Monoid a => a
mempty (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) []
newDimVar :: Usage -> Rigidity -> Name -> UnifyM VName
newDimVar Usage
usage Rigidity
rigidity Name
name = do
VName
dim <- Name -> UnifyM VName
newVar Name
name
case Rigidity
rigidity of
Rigid RigidSource
src ->
(Constraints -> Constraints) -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
-> (Constraints -> Constraints) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, Loc -> RigidSource -> Constraint
UnknownSize (Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage) RigidSource
src)
Rigidity
Nonrigid ->
(Constraints -> Constraints) -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
-> (Constraints -> Constraints) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$
VName -> (Int, Constraint) -> Constraints -> Constraints
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
dim (Int
0, Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing Usage
usage)
VName -> UnifyM VName
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim
curLevel :: UnifyM Int
curLevel = Int -> UnifyM Int
forall a. a -> UnifyM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
1
unifyError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> Doc () -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc ()
doc =
TypeError -> UnifyM a
forall a. TypeError -> UnifyM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (loc -> Loc
forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (Doc () -> TypeError) -> Doc () -> TypeError
forall a b. (a -> b) -> a -> b
$ Doc ()
doc Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs
matchError :: forall loc a.
Located loc =>
loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 =
TypeError -> UnifyM a
forall a. TypeError -> UnifyM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
forall a b. (a -> b) -> a -> b
$ Loc -> Notes -> Doc () -> TypeError
TypeError (loc -> Loc
forall a. Located a => a -> Loc
locOf loc
loc) Notes
notes (Doc () -> TypeError) -> Doc () -> TypeError
forall a b. (a -> b) -> a -> b
$ Doc ()
forall ann. Doc ann
doc Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BreadCrumbs -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. BreadCrumbs -> Doc ann
pretty BreadCrumbs
bcs
where
doc :: Doc a
doc =
Doc a
"Types"
Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t1)
Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
</> Doc a
"and"
Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
</> Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (StructType -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. StructType -> Doc ann
pretty StructType
t2)
Doc a -> Doc a -> Doc a
forall 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) =
Except TypeError a -> Either TypeError a
forall e a. Except e a -> Either e a
runExcept (Except TypeError a -> Either TypeError a)
-> Except TypeError a -> Either TypeError a
forall a b. (a -> b) -> a -> b
$ StateT (Constraints, Int) (Except TypeError) a
-> (Constraints, Int) -> Except TypeError a
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 =
[(VName, (Int, Constraint))] -> Constraints
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(VName, (Int, Constraint))] -> Constraints)
-> [(VName, (Int, Constraint))] -> Constraints
forall a b. (a -> b) -> a -> b
$
(TypeParam -> (VName, (Int, Constraint)))
-> [TypeParam] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> (VName, (Int, Constraint))
forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
nonrigid [TypeParam]
nonrigid_tparams [(VName, (Int, Constraint))]
-> [(VName, (Int, Constraint))] -> [(VName, (Int, Constraint))]
forall a. Semigroup a => a -> a -> a
<> (TypeParam -> (VName, (Int, Constraint)))
-> [TypeParam] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> (VName, (Int, Constraint))
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
1, Maybe Exp -> Usage -> Constraint
Size Maybe Exp
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> Loc -> Usage
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc))
nonrigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
1, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
l (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Usage) -> Loc -> Usage
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc))
rigid :: TypeParamBase a -> (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, Loc -> Constraint
ParamSize (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc))
rigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> Loc -> Constraint
ParamType Liftedness
l (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf 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 =
[TypeParam]
-> [TypeParam] -> UnifyM StructType -> Either TypeError StructType
forall a.
[TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams (UnifyM StructType -> Either TypeError StructType)
-> UnifyM StructType -> Either TypeError StructType
forall a b. (a -> b) -> a -> b
$ do
Usage -> StructType -> StructType -> UnifyM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (Maybe Text -> Loc -> Usage
Usage Maybe Text
forall a. Maybe a
Nothing (Loc -> Loc
forall a. Located a => a -> Loc
locOf Loc
loc)) StructType
t1 StructType
t2
StructType -> UnifyM StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2