{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
module Language.Futhark.TypeChecker.Unify
( Constraint (..),
Usage (..),
mkUsage,
mkUsage',
Level,
Constraints,
MonadUnify (..),
Rigidity (..),
RigidSource (..),
BreadCrumbs,
noBreadCrumbs,
hasNoBreadCrumbs,
dimNotes,
zeroOrderType,
arrayElemType,
mustHaveConstr,
mustHaveField,
mustBeOneOf,
equalityType,
normPatType,
normTypeFully,
instantiateEmptyArrayDims,
unify,
expect,
unifyMostCommon,
doUnification,
)
where
import Control.Monad.Except
import Control.Monad.State
import Data.Bifunctor
import Data.Char (isAscii)
import Data.List (foldl', intersect)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Util.Pretty hiding (empty)
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Types
data BreadCrumb
= MatchingTypes StructType StructType
| MatchingFields [Name]
| MatchingConstructor Name
| Matching Doc
instance Pretty BreadCrumb where
ppr :: BreadCrumb -> Doc
ppr (MatchingTypes StructType
t1 StructType
t2) =
Doc
"When matching type"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
Doc -> Doc -> Doc
</> Doc
"with"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t2)
ppr (MatchingFields [Name]
fields) =
Doc
"When matching types of record field"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote ([Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"." ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
ppr [Name]
fields) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
ppr (MatchingConstructor Name
c) =
Doc
"When matching types of constructor" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
ppr (Matching Doc
s) =
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 (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
ppr :: BreadCrumbs -> Doc
ppr (BreadCrumbs []) = Doc
forall a. Monoid a => a
mempty
ppr (BreadCrumbs [BreadCrumb]
bcs) = Doc
line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
stack ((BreadCrumb -> Doc) -> [BreadCrumb] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map BreadCrumb -> Doc
forall a. Pretty a => a -> Doc
ppr [BreadCrumb]
bcs)
data Usage = Usage (Maybe String) SrcLoc
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
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> Usage -> ShowS
Show)
mkUsage :: SrcLoc -> String -> Usage
mkUsage :: SrcLoc -> String -> Usage
mkUsage = (String -> SrcLoc -> Usage) -> SrcLoc -> String -> Usage
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe String -> SrcLoc -> Usage
Usage (Maybe String -> SrcLoc -> Usage)
-> (String -> Maybe String) -> String -> SrcLoc -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
forall a. a -> Maybe a
Just)
mkUsage' :: SrcLoc -> Usage
mkUsage' :: SrcLoc -> Usage
mkUsage' = Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing
instance Pretty Usage where
ppr :: Usage -> Doc
ppr (Usage Maybe String
Nothing SrcLoc
loc) = Doc
"use at " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
textwrap (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
loc)
ppr (Usage (Just String
s) SrcLoc
loc) = String -> Doc
textwrap String
s Doc -> Doc -> Doc
<+/> Doc
"at" Doc -> Doc -> Doc
<+> String -> Doc
textwrap (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
loc)
instance Located Usage where
locOf :: Usage -> Loc
locOf (Usage Maybe String
_ SrcLoc
loc) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc
type Level = Int
data Constraint
= NoConstraint Liftedness Usage
| ParamType Liftedness SrcLoc
| Constraint StructRetType Usage
| Overloaded [PrimType] Usage
| HasFields (M.Map Name StructType) Usage
| Equality Usage
| HasConstrs (M.Map Name [StructType]) Usage
| ParamSize SrcLoc
|
Size (Maybe Size) Usage
|
UnknowableSize SrcLoc RigidSource
deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show)
instance Located Constraint where
locOf :: Constraint -> Loc
locOf (NoConstraint Liftedness
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (ParamType Liftedness
_ SrcLoc
usage) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
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 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 Map Name [StructType]
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (ParamSize SrcLoc
loc) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc
locOf (Size Maybe Size
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
locOf (UnknowableSize SrcLoc
loc RigidSource
_) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc
type Constraints = M.Map VName (Level, Constraint)
lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
lookupSubst VName
v Constraints
constraints = case (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 Overloaded {} -> Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just Subst StructRetType
forall t. Subst t
PrimSubst
Just (Size (Just Size
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
$ Size -> Subst StructRetType
forall t. Size -> Subst t
SizeSubst (Size -> Subst StructRetType) -> Size -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d
Maybe Constraint
_ -> Maybe (Subst StructRetType)
forall a. Maybe a
Nothing
data RigidSource
=
RigidArg (Maybe (QualName VName)) String
|
RigidRet (Maybe (QualName VName))
| RigidLoop
|
RigidSlice (Maybe Size) String
|
RigidRange
|
RigidBound String
|
RigidCond StructType StructType
|
RigidUnify
| RigidOutOfScope SrcLoc VName
|
RigidCoerce
deriving (RigidSource -> RigidSource -> Bool
(RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool) -> Eq RigidSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RigidSource -> RigidSource -> Bool
$c/= :: RigidSource -> RigidSource -> Bool
== :: RigidSource -> RigidSource -> Bool
$c== :: RigidSource -> RigidSource -> Bool
Eq, Eq RigidSource
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
min :: RigidSource -> RigidSource -> RigidSource
$cmin :: RigidSource -> RigidSource -> RigidSource
max :: RigidSource -> RigidSource -> RigidSource
$cmax :: RigidSource -> RigidSource -> RigidSource
>= :: RigidSource -> RigidSource -> Bool
$c>= :: RigidSource -> RigidSource -> Bool
> :: RigidSource -> RigidSource -> Bool
$c> :: RigidSource -> RigidSource -> Bool
<= :: RigidSource -> RigidSource -> Bool
$c<= :: RigidSource -> RigidSource -> Bool
< :: RigidSource -> RigidSource -> Bool
$c< :: RigidSource -> RigidSource -> Bool
compare :: RigidSource -> RigidSource -> Ordering
$ccompare :: RigidSource -> RigidSource -> Ordering
$cp1Ord :: Eq 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
showList :: [RigidSource] -> ShowS
$cshowList :: [RigidSource] -> ShowS
show :: RigidSource -> String
$cshow :: RigidSource -> String
showsPrec :: Int -> RigidSource -> ShowS
$cshowsPrec :: Int -> RigidSource -> ShowS
Show)
data Rigidity = Rigid RigidSource | Nonrigid
deriving (Rigidity -> Rigidity -> Bool
(Rigidity -> Rigidity -> Bool)
-> (Rigidity -> Rigidity -> Bool) -> Eq Rigidity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c== :: Rigidity -> Rigidity -> Bool
Eq, Eq Rigidity
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
min :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmax :: Rigidity -> Rigidity -> Rigidity
>= :: Rigidity -> Rigidity -> Bool
$c>= :: Rigidity -> Rigidity -> Bool
> :: Rigidity -> Rigidity -> Bool
$c> :: Rigidity -> Rigidity -> Bool
<= :: Rigidity -> Rigidity -> Bool
$c<= :: Rigidity -> Rigidity -> Bool
< :: Rigidity -> Rigidity -> Bool
$c< :: Rigidity -> Rigidity -> Bool
compare :: Rigidity -> Rigidity -> Ordering
$ccompare :: Rigidity -> Rigidity -> Ordering
$cp1Ord :: Eq 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
showList :: [Rigidity] -> ShowS
$cshowList :: [Rigidity] -> ShowS
show :: Rigidity -> String
$cshow :: Rigidity -> String
showsPrec :: Int -> Rigidity -> ShowS
$cshowsPrec :: Int -> Rigidity -> ShowS
Show)
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet Maybe (QualName VName)
Nothing) =
Doc
"is unknown size returned by function at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet (Just QualName VName
fname)) =
Doc
"is unknown size returned by"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
fname)
Doc -> Doc -> Doc
<+> Doc
"at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidArg Maybe (QualName VName)
fname String
arg) =
Doc
"is value of argument"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
arg)
Doc -> Doc -> Doc
</> Doc
"passed to"
Doc -> Doc -> Doc
<+> Doc
fname'
Doc -> Doc -> Doc
<+> Doc
"at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
where
fname' :: Doc
fname' = Doc -> (QualName VName -> Doc) -> Maybe (QualName VName) -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" (Doc -> Doc
pquote (Doc -> Doc) -> (QualName VName -> Doc) -> QualName VName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr) Maybe (QualName VName)
fname
prettySource SrcLoc
ctx SrcLoc
loc (RigidSlice Maybe Size
d String
slice) =
Doc
"is size produced by slice"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
slice)
Doc -> Doc -> Doc
</> Doc
d_desc Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
where
d_desc :: Doc
d_desc = case Maybe Size
d of
Just Size
d' -> Doc
"of dimension of size " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d') Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" "
Maybe Size
Nothing -> Doc
forall a. Monoid a => a
mempty
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidLoop =
Doc
"is unknown size of value returned at" Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidRange =
Doc
"is unknown length of range at" Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidBound String
bound) =
Doc
"generated from expression"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
bound)
Doc -> Doc -> Doc
</> Doc
"used in range at " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidOutOfScope SrcLoc
boundloc VName
v) =
Doc
"is an unknown size arising from "
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName 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
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
Doc -> Doc -> Doc
</> Doc
"Originally bound at "
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
boundloc)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidCoerce =
Doc
"is an unknown size arising from empty dimension in coercion at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
_ SrcLoc
_ RigidSource
RigidUnify =
Doc
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource SrcLoc
ctx SrcLoc
loc (RigidCond StructType
t1 StructType
t2) =
Doc
"is unknown due to conditional expression at "
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
Doc -> Doc -> Doc
</> Doc
"One branch returns array of type: "
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
Doc -> Doc -> Doc
</> Doc
"The other an array of type: "
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t2)
dimNotes :: (Located a, MonadUnify m) => a -> Size -> m Notes
dimNotes :: a -> Size -> m Notes
dimNotes a
ctx (NamedSize QualName VName
d) = 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
_, UnknowableSize SrcLoc
loc RigidSource
rsrc) ->
Notes -> m Notes
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
. String -> Notes
forall a. Pretty a => a -> Notes
aNote (String -> Notes) -> (Doc -> String) -> Doc -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> m Notes) -> Doc -> m Notes
forall a b. (a -> b) -> a -> b
$
Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
d) Doc -> Doc -> Doc
<+> SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource (a -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf a
ctx) SrcLoc
loc RigidSource
rsrc
Maybe (Int, Constraint)
_ -> Notes -> m Notes
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty
dimNotes a
_ Size
_ = Notes -> m Notes
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 :: a -> StructType -> m Notes
typeNotes a
ctx =
([Notes] -> Notes) -> m [Notes] -> m Notes
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)
mapM (a -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes a
ctx (Size -> m Notes) -> (VName -> Size) -> VName -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize (QualName VName -> Size)
-> (VName -> QualName VName) -> VName -> Size
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
. StructType -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType
typeVarNotes :: MonadUnify m => VName -> m Notes
typeVarNotes :: 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 (Doc -> Notes
forall a. Pretty a => a -> Notes
aNote (Doc -> Notes)
-> ((Int, Constraint) -> Doc) -> (Int, Constraint) -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc
note (Constraint -> Doc)
-> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Doc
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 -> Doc
note (HasConstrs Map Name [StructType]
cs Usage
_) =
VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v
Doc -> Doc -> Doc
<+> Doc
"="
Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (((Name, [StructType]) -> Doc) -> [(Name, [StructType])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [StructType]) -> Doc
forall a b. Pretty a => (a, b) -> Doc
ppConstr (Map Name [StructType] -> [(Name, [StructType])]
forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
Doc -> Doc -> Doc
<+> Doc
"..."
note (Overloaded [PrimType]
ts Usage
_) =
VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v Doc -> Doc -> Doc
<+> Doc
"must be one of" Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts))
note (HasFields Map Name StructType
fs Usage
_) =
VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v
Doc -> Doc -> Doc
<+> Doc
"="
Doc -> Doc -> Doc
<+> Doc -> Doc
braces ([Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " (((Name, StructType) -> Doc) -> [(Name, StructType)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, StructType) -> Doc
forall v b. IsName v => (v, b) -> Doc
ppField (Map Name StructType -> [(Name, StructType)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs))))
note Constraint
_ = Doc
forall a. Monoid a => a
mempty
ppConstr :: (a, b) -> Doc
ppConstr (a
c, b
_) = Doc
"#" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> a -> Doc
forall a. Pretty a => a -> Doc
ppr a
c Doc -> Doc -> Doc
<+> Doc
"..." Doc -> Doc -> Doc
<+> Doc
"|"
ppField :: (v, b) -> Doc
ppField (v
f, b
_) = v -> Doc
forall v. IsName v => v -> Doc
pprName v
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
":" Doc -> Doc -> Doc
<+> Doc
"..."
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 => SrcLoc -> Name -> m (TypeBase dim als)
newDimVar :: SrcLoc -> Rigidity -> Name -> m VName
curLevel :: m Level
matchError ::
Located loc =>
loc ->
Notes ->
BreadCrumbs ->
StructType ->
StructType ->
m a
unifyError ::
Located loc =>
loc ->
Notes ->
BreadCrumbs ->
Doc ->
m a
normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a
normTypeFully :: a -> m a
normTypeFully a
t = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
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 :: StructType -> m StructType
normType t :: StructType
t@(Scalar (TypeVar ()
_ Uniqueness
_ (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 (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
normType StructType
t = StructType -> m StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
normPatType :: MonadUnify m => PatType -> m PatType
normPatType :: PatType -> m PatType
normPatType t :: PatType
t@(Scalar (TypeVar Aliasing
als Uniqueness
u (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
_) ->
PatType -> m PatType
forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType (PatType -> m PatType) -> PatType -> m PatType
forall a b. (a -> b) -> a -> b
$ StructType
t' StructType -> Uniqueness -> StructType
forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
u StructType -> Aliasing -> PatType
forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` Aliasing
als
Maybe Constraint
_ -> PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t
normPatType PatType
t = PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t
rigidConstraint :: Constraint -> Bool
rigidConstraint :: Constraint -> Bool
rigidConstraint ParamType {} = Bool
True
rigidConstraint ParamSize {} = Bool
True
rigidConstraint UnknowableSize {} = Bool
True
rigidConstraint Constraint
_ = Bool
False
instantiateEmptyArrayDims ::
MonadUnify m =>
SrcLoc ->
Rigidity ->
RetTypeBase Size als ->
m (TypeBase Size als, [VName])
instantiateEmptyArrayDims :: SrcLoc
-> Rigidity
-> RetTypeBase Size als
-> m (TypeBase Size als, [VName])
instantiateEmptyArrayDims SrcLoc
tloc Rigidity
r (RetType [VName]
dims TypeBase Size als
t) = do
[VName]
dims' <- (VName -> m VName) -> [VName] -> m [VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> m VName
new [VName]
dims
(TypeBase Size als, [VName]) -> m (TypeBase Size als, [VName])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Size -> Size) -> TypeBase Size als -> TypeBase Size als
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(VName, VName)] -> Size -> Size
onDim ([(VName, VName)] -> Size -> Size)
-> [(VName, VName)] -> Size -> Size
forall a b. (a -> b) -> a -> b
$ [VName] -> [VName] -> [(VName, VName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims [VName]
dims') TypeBase Size als
t, [VName]
dims')
where
new :: VName -> m VName
new = SrcLoc -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
tloc Rigidity
r (Name -> m VName) -> (VName -> Name) -> VName -> m VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
nameFromString (String -> Name) -> (VName -> String) -> VName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii ShowS -> (VName -> String) -> VName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> String
baseString
onDim :: [(VName, VName)] -> Size -> Size
onDim [(VName, VName)]
dims' (NamedSize QualName VName
d) =
QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ QualName VName
-> (VName -> QualName VName) -> Maybe VName -> QualName VName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe QualName VName
d VName -> QualName VName
forall v. v -> QualName v
qualName (VName -> [(VName, VName)] -> Maybe VName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) [(VName, VName)]
dims')
onDim [(VName, VName)]
_ Size
d = Size
d
isRigid :: VName -> Constraints -> Bool
isRigid :: VName -> Constraints -> Bool
isRigid VName
v Constraints
constraints =
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 (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl
type UnifyDims m =
BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Size -> Size -> m ()
flipUnifyDims :: UnifyDims m -> UnifyDims m
flipUnifyDims :: UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t1 Size
t2 =
UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t2 Size
t1
unifyWith ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
StructType ->
StructType ->
m ()
unifyWith :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage = Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
False
where
swap :: Bool -> a -> a -> (a, a)
swap Bool
True a
x a
y = (a
y, a
x)
swap Bool
False a
x a
y = (a
x, a
y)
subunify :: Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs StructType
t1 StructType
t2 = do
Constraints
constraints <- 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 (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' =
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims m
linkDims Usage
usage [VName]
bound BreadCrumbs
bcs
where
linkDims :: UnifyDims m
linkDims
| Bool
ord' = UnifyDims m -> UnifyDims m
forall (m :: * -> *). UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims
| Bool
otherwise = UnifyDims m
onDims
unifyTypeArg :: BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Size
d1 SrcLoc
_) (TypeArgDim Size
d2 SrcLoc
_) =
BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (Bool -> Size -> Size -> (Size, Size)
forall a. Bool -> a -> a -> (a, a)
swap Bool
ord Size
d1 Size
d2)
unifyTypeArg BreadCrumbs
bcs' (TypeArgType StructType
t SrcLoc
_) (TypeArgType StructType
arg_t SrcLoc
_) =
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
t StructType
arg_t
unifyTypeArg BreadCrumbs
bcs' TypeArg Size
_ TypeArg Size
_ =
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (Size
d1, Size
d2) =
UnifyDims m
onDims
BreadCrumbs
bcs'
[VName]
bound
VName -> Maybe Int
nonrigid
(TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d1)
(TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d2)
case (StructType
t1', StructType
t2') of
( Scalar (Record Map Name StructType
fs),
Scalar (Record Map Name StructType
arg_fs)
)
| 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 ->
[(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
fs Map Name StructType
arg_fs) (((Name, (StructType, StructType)) -> m ()) -> m ())
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Name
k, (StructType
k_t1, StructType
k_t2)) -> do
let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
k]) BreadCrumbs
bcs
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
k_t1 StructType
k_t2
| Bool
otherwise -> do
let missing :: [Name]
missing =
(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 (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
<+> [Doc] -> Doc
commasep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
ppr [Name]
missing) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Size]
targs),
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Size]
arg_targs)
)
| VName
tn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
[TypeArg Size] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
targs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Size] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
arg_targs -> do
let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc -> BreadCrumb
Matching Doc
"When matching type arguments.") BreadCrumbs
bcs
(TypeArg Size -> TypeArg Size -> m ())
-> [TypeArg Size] -> [TypeArg Size] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Size]
targs [TypeArg Size]
arg_targs
( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v1) []),
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v2) [])
) ->
case (VName -> Maybe Int
nonrigid VName
v1, VName -> Maybe Int
nonrigid VName
v2) of
(Maybe Int
Nothing, Maybe Int
Nothing) -> 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 ()
_ Uniqueness
_ (QualName [] VName
v1) []), StructType
_)
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v1 ->
Bool -> VName -> Int -> StructType -> m ()
link Bool
ord VName
v1 Int
lvl StructType
t2'
(StructType
_, Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v2) []))
| Just Int
lvl <- VName -> Maybe Int
nonrigid VName
v2 ->
Bool -> VName -> Int -> StructType -> m ()
link (Bool -> Bool
not Bool
ord) VName
v2 Int
lvl StructType
t1'
( Scalar (Arrow ()
_ PName
p1 StructType
a1 (RetType [VName]
b1_dims StructType
b1)),
Scalar (Arrow ()
_ PName
p2 StructType
a2 (RetType [VName]
b2_dims StructType
b2))
) -> do
let (Constraint
r1, Constraint
r2) =
Bool -> Constraint -> Constraint -> (Constraint, Constraint)
forall a. Bool -> a -> a -> (a, a)
swap
Bool
ord
(Maybe Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
forall a. Monoid a => a
mempty)
(SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
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] -> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b1_dims ([(Int, Constraint)] -> [(VName, (Int, Constraint))])
-> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> a -> b
$ (Int, Constraint) -> [(Int, Constraint)]
forall a. a -> [a]
repeat (Int
lvl, Constraint
r1)) Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<>)
(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] -> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b2_dims ([(Int, Constraint)] -> [(VName, (Int, Constraint))])
-> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> a -> b
$ (Int, Constraint) -> [(Int, Constraint)]
forall a. a -> [a]
repeat (Int
lvl, Constraint
r2)) Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<>)
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)
StructType
b1'
StructType
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 (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
(StructType
b1', StructType
b2') =
case (PName
p1, PName
p2) of
(Named VName
p1', Named VName
p2') ->
let f :: VName -> Maybe (Subst t)
f VName
v
| VName
v 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
$ Size -> Subst t
forall t. Size -> Subst t
SizeSubst (Size -> Subst t) -> Size -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
p1'
| Bool
otherwise = Maybe (Subst t)
forall a. Maybe a
Nothing
in (StructType
b1, TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall t. VName -> Maybe (Subst t)
f StructType
b2)
(PName
_, PName
_) ->
(StructType
b1, StructType
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 (Size
t1_d : [Size]
_) <- StructType -> Shape Size
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t1',
Shape (Size
t2_d : [Size]
_) <- StructType -> Shape Size
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t2',
Just StructType
t1'' <- Int -> StructType -> Maybe StructType
forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t1',
Just StructType
t2'' <- Int -> StructType -> Maybe StructType
forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t2' -> do
BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs (Bool -> Size -> Size -> (Size, Size)
forall a. Bool -> a -> a -> (a, a)
swap Bool
ord Size
t1_d Size
t2_d)
Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs StructType
t1'' StructType
t2''
( Scalar (Sum Map Name [StructType]
cs),
Scalar (Sum Map Name [StructType]
arg_cs)
)
| 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 ->
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs Map Name [StructType]
arg_cs
| Bool
otherwise -> do
let missing :: [Name]
missing =
(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_cs) (Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs)
[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]
cs) (Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs)
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 constructors:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"#" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
ppr) [Name]
missing) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
(StructType, StructType)
_
| StructType
t1' StructType -> StructType -> Bool
forall a. Eq a => a -> a -> Bool
== StructType
t2' -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
| Bool
otherwise -> m ()
forall a. m a
failure
unifyDims :: MonadUnify m => Usage -> UnifyDims m
unifyDims :: Usage -> UnifyDims m
unifyDims Usage
_ BreadCrumbs
_ [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2
| Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
| Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1 =
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
| Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2 =
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2 = do
Notes
notes <- 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 -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 m (Notes -> Notes) -> m Notes -> m Notes
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Usage -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
"Dimensions"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d1)
Doc -> Doc -> Doc
<+> Doc
"and"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d2)
Doc -> Doc -> Doc
<+> Doc
"do not match."
unify :: MonadUnify m => Usage -> StructType -> StructType -> m ()
unify :: Usage -> StructType -> StructType -> m ()
unify Usage
usage = UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith (Usage -> UnifyDims m
forall (m :: * -> *). MonadUnify m => Usage -> UnifyDims m
unifyDims Usage
usage) Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
expect :: MonadUnify m => Usage -> StructType -> StructType -> m ()
expect :: Usage -> StructType -> StructType -> m ()
expect Usage
usage = UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
forall (f :: * -> *) (t :: * -> *).
(Foldable t, MonadUnify f) =>
BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
where
onDims :: BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims BreadCrumbs
_ t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2
| Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
| Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1,
Bool -> Bool
not (t VName -> Size -> Bool
forall (t :: * -> *). Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d2) Bool -> Bool -> Bool
|| (VName
d1 VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
Usage -> BreadCrumbs -> VName -> Int -> Size -> f ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
| Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2,
Bool -> Bool
not (t VName -> Size -> Bool
forall (t :: * -> *). Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d1) Bool -> Bool -> Bool
|| (VName
d2 VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
Usage -> BreadCrumbs -> VName -> Int -> Size -> f ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
onDims BreadCrumbs
bcs t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2 = do
Notes
notes <- Notes -> Notes -> Notes
forall a. Semigroup a => a -> a -> a
(<>) (Notes -> Notes -> Notes) -> f Notes -> f (Notes -> Notes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Usage -> Size -> f Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 f (Notes -> Notes) -> f Notes -> f Notes
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Usage -> Size -> f Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
Usage -> Notes -> BreadCrumbs -> Doc -> f ()
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc -> f ()) -> Doc -> f ()
forall a b. (a -> b) -> a -> b
$
Doc
"Dimensions"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d1)
Doc -> Doc -> Doc
<+> Doc
"and"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d2)
Doc -> Doc -> Doc
<+> Doc
"do not match."
boundParam :: t VName -> Size -> Bool
boundParam t VName
bound (NamedSize (QualName [VName]
_ VName
d)) = VName
d VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound
boundParam t VName
_ Size
_ = Bool
False
occursCheck ::
MonadUnify m =>
Usage ->
BreadCrumbs ->
VName ->
StructType ->
m ()
occursCheck :: 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 as dim. Monoid 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 (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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
Doc -> Doc -> Doc
<+> Doc
"with"
Doc -> Doc -> Doc
<+> StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
scopeCheck ::
MonadUnify m =>
Usage ->
BreadCrumbs ->
VName ->
Level ->
StructType ->
m ()
scopeCheck :: 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 :: * -> *) as.
(MonadUnify m, Monoid as) =>
Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints StructType
tp
where
checkType :: Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints TypeBase Size as
t =
(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 Size as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size as
t Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> TypeBase Size as -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType TypeBase Size as
t
check :: Constraints -> VName -> m ()
check Constraints
constraints VName
v
| Just (Int
lvl, Constraint
c) <- 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 (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 (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
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
Doc -> Doc -> Doc
</> Doc
"with"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
Doc -> Doc -> Doc
</> Doc
"This is because"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (v -> Doc
forall v. IsName v => v -> Doc
pprName v
v)
Doc -> Doc -> Doc
<+> Doc
"is rigidly bound in a deeper scope."
linkVarToType ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
VName ->
Level ->
StructType ->
m ()
linkVarToType :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs VName
vn Int
lvl StructType
tp_unnorm = do
StructType
tp <- 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 (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
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
commasep ((VName -> Doc) -> [VName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
pquote (Doc -> Doc) -> (VName -> Doc) -> VName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Doc
forall v. IsName v => v -> Doc
pprName) [VName]
problems)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" used as size(s) would go out of scope."
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
let bcs' :: BreadCrumbs
bcs' =
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> String -> Doc
textwrap String
"is not instantiated with a function type, due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
unlift_usage
)
BreadCrumbs
bcs
m ()
link
Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs' 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) (StructType -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType StructType
tp)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
Doc -> Doc -> Doc
<+> Doc
"cannot be instantiated with type containing anonymous sizes:"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
Doc -> Doc -> Doc
</> String -> Doc
textwrap String
"This is usually because the size of an array returned by a higher-order function argument cannot be determined statically. This can also be due to the return size being a value parameter. Add type annotation to clarify."
Just (Equality Usage
_) -> do
m ()
link
Usage -> StructType -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage StructType
tp
Just (Overloaded [PrimType]
ts Usage
old_usage)
| StructType
tp 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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> (PrimType -> ScalarTypeBase Size ()) -> PrimType -> StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimType -> ScalarTypeBase Size ()
forall dim as. PrimType -> ScalarTypeBase dim as
Prim) [PrimType]
ts -> do
m ()
link
case StructType
tp of
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v) [])
| Bool -> Bool
not (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 (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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"with type"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
Doc -> Doc -> Doc
</> Doc
"as"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"must be one of"
Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
Doc -> Doc -> Doc
<+/> Doc
"due to"
Doc -> Doc -> Doc
<+/> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
Just (HasFields Map Name StructType
required_fields Usage
old_usage) -> do
m ()
link
case StructType
tp of
Scalar (Record Map Name StructType
tp_fields)
| (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)
mapM StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully Map Name StructType
required_fields
let bcs' :: BreadCrumbs
bcs' =
BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
( Doc -> BreadCrumb
Matching (Doc -> BreadCrumb) -> Doc -> BreadCrumb
forall a b. (a -> b) -> a -> b
$
VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
Doc -> Doc -> Doc
<+> Doc
"must be a record with at least the fields:"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (ScalarTypeBase Size () -> Doc
forall a. Pretty a => a -> Doc
ppr (Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields'))
Doc -> Doc -> Doc
</> Doc
"due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
)
BreadCrumbs
bcs
((StructType, StructType) -> m ())
-> [(StructType, StructType)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((StructType -> StructType -> m ())
-> (StructType, StructType) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((StructType -> StructType -> m ())
-> (StructType, StructType) -> m ())
-> (StructType -> StructType -> m ())
-> (StructType, StructType)
-> m ()
forall a b. (a -> b) -> a -> b
$ UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') ([(StructType, StructType)] -> m ())
-> [(StructType, StructType)] -> m ()
forall a b. (a -> b) -> a -> b
$
Map Name (StructType, StructType) -> [(StructType, StructType)]
forall k a. Map k a -> [a]
M.elems (Map Name (StructType, StructType) -> [(StructType, StructType)])
-> Map Name (StructType, StructType) -> [(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
required_fields Map Name StructType
tp_fields
Scalar (TypeVar ()
_ Uniqueness
_ (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 ->
(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
lvl, Map Name StructType -> Usage -> Constraint
HasFields Map Name StructType
required_fields Usage
old_usage)
StructType
_ ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"with type"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
Doc -> Doc -> Doc
</> Doc
"as"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"must be a record with fields"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (ScalarTypeBase Size () -> Doc
forall a. Pretty a => a -> Doc
ppr (Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields))
Doc -> Doc -> Doc
</> Doc
"due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
Just (HasConstrs Map Name [StructType]
required_cs Usage
old_usage) ->
case StructType
tp of
Scalar (Sum Map Name [StructType]
ts)
| (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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Size ()
forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum (Map Name [StructType] -> ScalarTypeBase Size ())
-> Map Name [StructType] -> ScalarTypeBase Size ()
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` StructType -> Set VName
forall as. TypeBase Size as -> Set VName
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)
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
ts
Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v) []) -> do
case 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 Map Name [StructType]
v_cs Usage
_) -> do
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
v_cs
Just (Int
_, NoConstraint {}) -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, Equality {}) -> () -> m ()
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 (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, Map Name [StructType] -> Usage -> Constraint
HasConstrs Map Name [StructType]
required_cs Usage
old_usage)
where
combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs (Int
_, HasConstrs Map Name [StructType]
cs1 Usage
usage1) (a
_, HasConstrs Map Name [StructType]
cs2 Usage
_) =
(Int
lvl, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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
forall a. Monoid a => a
mempty
Maybe Constraint
_ -> m ()
link
where
noSumType :: Notes -> m a
noSumType Notes
notes =
Usage -> 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"
linkVarToDim ::
MonadUnify m =>
Usage ->
BreadCrumbs ->
VName ->
Level ->
Size ->
m ()
linkVarToDim :: Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
vn Int
lvl Size
dim = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
case Size
dim of
NamedSize QualName VName
dim'
| Just (Int
dim_lvl, Constraint
c) <- QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName 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 -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
dim
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 unify size variable"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
Doc -> Doc -> Doc
<+> Doc
"with"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
Doc -> Doc -> Doc
</> Doc
"This is because"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
Doc -> Doc -> Doc
<+> Doc
"is rigidly bound in a deeper scope."
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 (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
dim') (Int
lvl, Constraint
c)
Size
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
(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 Size -> Usage -> Constraint
Size (Size -> Maybe Size
forall a. a -> Maybe a
Just Size
dim) Usage
usage)
mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m ()
mustBeOneOf :: [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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (PrimType -> ScalarTypeBase Size ()
forall dim as. PrimType -> ScalarTypeBase dim as
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 ()
_ Uniqueness
_ (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ts -> () -> m ()
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 (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
$
String -> Doc
text String
"Cannot unify type"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t)
Doc -> Doc -> Doc
<+> Doc
"with any of " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
linkVarToTypes :: MonadUnify m => Usage -> VName -> [PrimType] -> m ()
linkVarToTypes :: 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 (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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
Doc -> Doc -> Doc
<+> Doc
"but also one of"
Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
vn_ts)
Doc -> Doc -> Doc
<+> Doc
"due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr 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 Map Name [StructType]
_ Usage
vn_usage) ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [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
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
vn_usage
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
Just (Int
_, HasFields Map Name StructType
_ Usage
vn_usage) ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
", but also inferred to be record due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr 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 (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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
equalityType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
TypeBase dim as ->
m ()
equalityType :: Usage -> TypeBase dim as -> m ()
equalityType Usage
usage TypeBase dim as
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
<+> Doc
"does not support equality (is higher-order)."
(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 as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase dim as
t
where
mustBeEquality :: VName -> m ()
mustBeEquality VName
vn = do
Constraints
constraints <- 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 ()
_ Uniqueness
_ (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 (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
<+> Doc -> Doc
pquote (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t)
Doc -> Doc -> Doc
<+> Doc
"does not support equality."
Doc -> Doc -> Doc
</> Doc
"Constrained to be higher-order due to"
Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
cusage
Doc -> Doc -> Doc
<+> Doc
"."
| Bool
otherwise -> () -> m ()
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 (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, Equality {}) ->
() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just (Int
_, HasConstrs Map Name [StructType]
cs Usage
_) ->
(StructType -> m ()) -> [StructType] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Usage -> StructType -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage) ([StructType] -> m ()) -> [StructType] -> m ()
forall a b. (a -> b) -> a -> b
$ [[StructType]] -> [StructType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[StructType]] -> [StructType]) -> [[StructType]] -> [StructType]
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> [[StructType]]
forall k a. Map k a -> [a]
M.elems Map Name [StructType]
cs
Maybe (Int, Constraint)
_ ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn Doc -> Doc -> Doc
<+> Doc
"does not support equality."
zeroOrderTypeWith ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
BreadCrumbs ->
TypeBase dim as ->
m ()
zeroOrderTypeWith :: Usage -> BreadCrumbs -> TypeBase dim as -> m ()
zeroOrderTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
</> Int -> Doc -> Doc
indent Int
2 (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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 as -> [VName]) -> TypeBase dim as -> 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 as -> Set VName) -> TypeBase dim as -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars (TypeBase dim as -> m ()) -> TypeBase dim as -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim as
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
Lifted SrcLoc
ploc) ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
ploc)
Doc -> Doc -> Doc
<+> Doc
"may be a function."
Maybe (Int, Constraint)
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
zeroOrderType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
String ->
TypeBase dim as ->
m ()
zeroOrderType :: Usage -> String -> TypeBase dim as -> m ()
zeroOrderType Usage
usage String
desc =
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
zeroOrderTypeWith Usage
usage (BreadCrumbs -> TypeBase dim as -> m ())
-> BreadCrumbs -> TypeBase dim as -> 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
<+> String -> Doc
textwrap String
desc
arrayElemTypeWith ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
BreadCrumbs ->
TypeBase dim as ->
m ()
arrayElemTypeWith :: Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
</> Int -> Doc -> Doc
indent Int
2 (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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 as -> [VName]) -> TypeBase dim as -> 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 as -> Set VName) -> TypeBase dim as -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars (TypeBase dim as -> m ()) -> TypeBase dim as -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim as
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 SrcLoc
ploc)
| Liftedness
l Liftedness -> [Liftedness] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Liftedness
Lifted, Liftedness
SizeLifted] ->
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
Doc -> Doc -> Doc
<+> Doc
"bound at"
Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
ploc)
Doc -> Doc -> Doc
<+> Doc
"is lifted and cannot be an array element."
Maybe (Int, Constraint)
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
arrayElemType ::
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage ->
String ->
TypeBase dim as ->
m ()
arrayElemType :: Usage -> String -> TypeBase dim as -> m ()
arrayElemType Usage
usage String
desc =
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage (BreadCrumbs -> TypeBase dim as -> m ())
-> BreadCrumbs -> TypeBase dim as -> 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
<+> String -> Doc
textwrap String
desc
unifySharedConstructors ::
MonadUnify m =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
M.Map Name [StructType] ->
M.Map Name [StructType] ->
m ()
unifySharedConstructors :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs1 Map Name [StructType]
cs2 =
[(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 (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> 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_ (UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') [StructType]
f1 [StructType]
f2
| Bool
otherwise =
Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (Name -> Doc
forall v. IsName v => v -> Doc
pprName Name
c) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
mustHaveConstr ::
MonadUnify m =>
Usage ->
Name ->
StructType ->
[StructType] ->
m ()
mustHaveConstr :: 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 ()
_ Uniqueness
_ (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
(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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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 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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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 (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> 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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr 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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> Doc
"not present in type."
Just [StructType]
fs'
| [StructType] -> 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 (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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> 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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Size ()
forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum (Map Name [StructType] -> ScalarTypeBase Size ())
-> Map Name [StructType] -> ScalarTypeBase Size ()
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 =>
UnifyDims m ->
Usage ->
[VName] ->
BreadCrumbs ->
Name ->
PatType ->
m PatType
mustHaveFieldWith :: UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
mustHaveFieldWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l PatType
t = do
Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
StructType
l_type <- SrcLoc -> Name -> m StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Name
"t"
let l_type' :: PatType
l_type' = StructType
l_type StructType -> Aliasing -> PatType
forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` PatType -> Aliasing
forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
case PatType
t of
Scalar (TypeVar Aliasing
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [])
| Just (Int
lvl, NoConstraint {}) <- 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, Map Name StructType -> Usage -> Constraint
HasFields (Name -> StructType -> Map Name StructType
forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type) Usage
usage)
PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
| Just (Int
lvl, HasFields 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' -> UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs StructType
l_type StructType
t'
Maybe StructType
Nothing ->
(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, Map Name StructType -> Usage -> Constraint
HasFields (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)
PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
Scalar (Record Map Name PatType
fields)
| Just PatType
t' <- Name -> Map Name PatType -> Maybe PatType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name PatType
fields -> do
Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
l_type (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t'
PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t'
| Bool
otherwise ->
Usage -> Notes -> BreadCrumbs -> Doc -> m PatType
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 PatType) -> Doc -> m PatType
forall a b. (a -> b) -> a -> b
$
Doc
"Attempt to access field"
Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
l)
Doc -> Doc -> Doc
<+> Doc
" of value of type"
Doc -> Doc -> Doc
<+> TypeBase () () -> Doc
forall a. Pretty a => a -> Doc
ppr (PatType -> TypeBase () ()
forall dim as. TypeBase dim as -> TypeBase () ()
toStructural PatType
t) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
PatType
_ -> do
Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record (Map Name StructType -> ScalarTypeBase Size ())
-> Map Name StructType -> ScalarTypeBase Size ()
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
PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
mustHaveField ::
MonadUnify m =>
Usage ->
Name ->
PatType ->
m PatType
mustHaveField :: Usage -> Name -> PatType -> m PatType
mustHaveField Usage
usage = UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
mustHaveFieldWith (Usage -> UnifyDims m
forall (m :: * -> *). MonadUnify m => Usage -> UnifyDims m
unifyDims Usage
usage) Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
newDimOnMismatch ::
(Monoid as, MonadUnify m) =>
SrcLoc ->
TypeBase Size as ->
TypeBase Size as ->
m (TypeBase Size as, [VName])
newDimOnMismatch :: SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch SrcLoc
loc TypeBase Size as
t1 TypeBase Size as
t2 = do
(TypeBase Size as
t, Map (Size, Size) VName
seen) <- StateT (Map (Size, Size) VName) m (TypeBase Size as)
-> Map (Size, Size) VName
-> m (TypeBase Size as, Map (Size, Size) VName)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (([VName] -> Size -> Size -> StateT (Map (Size, Size) VName) m Size)
-> TypeBase Size as
-> TypeBase Size as
-> StateT (Map (Size, Size) VName) m (TypeBase Size as)
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] -> Size -> Size -> StateT (Map (Size, Size) VName) m Size
forall (t :: (* -> *) -> * -> *) (m :: * -> *) p.
(MonadState (Map (Size, Size) VName) (t m), MonadTrans t,
MonadUnify m) =>
p -> Size -> Size -> t m Size
onDims TypeBase Size as
t1 TypeBase Size as
t2) Map (Size, Size) VName
forall a. Monoid a => a
mempty
(TypeBase Size as, [VName]) -> m (TypeBase Size as, [VName])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size as
t, Map (Size, Size) VName -> [VName]
forall k a. Map k a -> [a]
M.elems Map (Size, Size) VName
seen)
where
r :: Rigidity
r = RigidSource -> Rigidity
Rigid (RigidSource -> Rigidity) -> RigidSource -> Rigidity
forall a b. (a -> b) -> a -> b
$ StructType -> StructType -> RigidSource
RigidCond (TypeBase Size as -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t1) (TypeBase Size as -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t2)
onDims :: p -> Size -> Size -> t m Size
onDims p
_ Size
d1 Size
d2
| Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d1
| Bool
otherwise = do
Maybe VName
maybe_d <- (Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName))
-> (Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName)
forall a b. (a -> b) -> a -> b
$ (Size, Size) -> Map (Size, Size) VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Size
d1, Size
d2)
case Maybe VName
maybe_d of
Just VName
d -> Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> t m Size) -> Size -> t m Size
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
d
Maybe VName
Nothing -> do
VName
d <- m VName -> t m VName
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
$ SrcLoc -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
"differ"
(Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ())
-> (Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ()
forall a b. (a -> b) -> a -> b
$ (Size, Size)
-> VName -> Map (Size, Size) VName -> Map (Size, Size) VName
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Size
d1, Size
d2) VName
d
Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> t m Size) -> Size -> t m Size
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
d
unifyMostCommon ::
MonadUnify m =>
Usage ->
PatType ->
PatType ->
m (PatType, [VName])
unifyMostCommon :: Usage -> PatType -> PatType -> m (PatType, [VName])
unifyMostCommon Usage
usage PatType
t1 PatType
t2 = do
let allOK :: p -> p -> p -> p -> p -> f ()
allOK p
_ p
_ p
_ p
_ p
_ = () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t1) (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t2)
PatType
t1' <- PatType -> m PatType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t1
PatType
t2' <- PatType -> m PatType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t2
SrcLoc -> PatType -> PatType -> m (PatType, [VName])
forall as (m :: * -> *).
(Monoid as, MonadUnify m) =>
SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) PatType
t1' PatType
t2'
type UnifyMState = (Constraints, Int)
newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
deriving
( Applicative UnifyM
a -> UnifyM a
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
UnifyM a -> (a -> UnifyM b) -> UnifyM b
UnifyM a -> UnifyM b -> UnifyM b
forall a. a -> UnifyM a
forall a b. UnifyM a -> UnifyM b -> UnifyM b
forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> UnifyM a
$creturn :: forall a. a -> UnifyM a
>> :: UnifyM a -> UnifyM b -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>>= :: UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$cp1Monad :: Applicative UnifyM
Monad,
a -> UnifyM b -> UnifyM a
(a -> b) -> UnifyM a -> UnifyM b
(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
<$ :: a -> UnifyM b -> UnifyM a
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
fmap :: (a -> b) -> UnifyM a -> UnifyM b
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
Functor,
Functor UnifyM
a -> UnifyM a
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
UnifyM a -> UnifyM b -> UnifyM b
UnifyM a -> UnifyM b -> UnifyM a
UnifyM (a -> b) -> UnifyM a -> UnifyM b
(a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
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
<* :: UnifyM a -> UnifyM b -> UnifyM a
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
*> :: UnifyM a -> UnifyM b -> UnifyM b
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
liftA2 :: (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
<*> :: UnifyM (a -> b) -> UnifyM a -> UnifyM b
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
pure :: a -> UnifyM a
$cpure :: forall a. a -> UnifyM a
$cp1Applicative :: Functor UnifyM
Applicative,
MonadState UnifyMState,
MonadError TypeError
)
newVar :: Name -> UnifyM VName
newVar :: Name -> UnifyM VName
newVar Name
name = do
(Constraints
x, Int
i) <- UnifyM UnifyMState
forall s (m :: * -> *). MonadState s m => m s
get
UnifyMState -> 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 (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 = (UnifyMState -> Constraints) -> UnifyM Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnifyMState -> Constraints
forall a b. (a, b) -> a
fst
putConstraints :: Constraints -> UnifyM ()
putConstraints Constraints
x = (UnifyMState -> UnifyMState) -> UnifyM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UnifyMState -> UnifyMState) -> UnifyM ())
-> (UnifyMState -> UnifyMState) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ \(Constraints
_, Int
i) -> (Constraints
x, Int
i)
newTypeVar :: SrcLoc -> Name -> UnifyM (TypeBase dim als)
newTypeVar SrcLoc
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 String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc)
TypeBase dim als -> UnifyM (TypeBase dim als)
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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase dim als -> TypeBase dim als)
-> ScalarTypeBase dim als -> TypeBase dim als
forall a b. (a -> b) -> a -> b
$ als
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim als
forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar als
forall a. Monoid a => a
mempty Uniqueness
Nonunique (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) []
newDimVar :: SrcLoc -> Rigidity -> Name -> UnifyM VName
newDimVar SrcLoc
loc Rigidity
rigidity Name
name = do
VName
dim <- Name -> UnifyM VName
newVar Name
name
case Rigidity
rigidity of
Rigid RigidSource
src -> (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, SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
loc 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 Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc)
VName -> UnifyM VName
forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim
curLevel :: UnifyM Int
curLevel = Int -> UnifyM Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
unifyError :: loc -> Notes -> BreadCrumbs -> Doc -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc
doc =
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. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
matchError :: loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 =
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. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
where
doc :: Doc
doc =
Doc
"Types"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
Doc -> Doc -> Doc
</> Doc
"and"
Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t2)
Doc -> Doc -> Doc
</> Doc
"do not match."
runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams (UnifyM StateT UnifyMState (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 UnifyMState (Except TypeError) a
-> UnifyMState -> Except TypeError a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT UnifyMState (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
0, Maybe Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc))
nonrigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
l (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc))
rigid :: TypeParamBase a -> (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, SrcLoc -> Constraint
ParamSize SrcLoc
loc))
rigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc))
doUnification ::
Loc ->
[TypeParam] ->
[TypeParam] ->
StructType ->
StructType ->
Either TypeError StructType
doUnification :: Loc
-> [TypeParam]
-> [TypeParam]
-> StructType
-> StructType
-> Either TypeError StructType
doUnification Loc
loc [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams StructType
t1 StructType
t2 =
[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 ()
expect (Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing (Loc -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Loc
loc)) StructType
t1 StructType
t2
StructType -> UnifyM StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully StructType
t2