module Language.Futhark.TypeChecker.Terms.Pat
( binding,
bindingParams,
bindingPat,
bindingIdent,
bindingSizes,
doNotShadow,
)
where
import Control.Monad
import Control.Monad.State
import Data.Bitraversable
import Data.Either
import Data.List (find, isPrefixOf, sort)
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Data.Text qualified as T
import Futhark.Util.Pretty hiding (group, space)
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Terms.Monad
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify hiding (Usage)
import Prelude hiding (mod)
doNotShadow :: [Name]
doNotShadow :: [Name]
doNotShadow = [Name
"&&", Name
"||"]
nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor [] StructType
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
nonrigidFor [SizeBinder VName]
sizes StructType
t = forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall {t :: (* -> *) -> * -> *} {f :: * -> *}.
(MonadState [(VName, VName)] (t TermTypeM), MonadTrans t) =>
ExpBase f VName -> t TermTypeM (ExpBase f VName)
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t) forall a. Monoid a => a
mempty
where
onDim :: ExpBase f VName -> t TermTypeM (ExpBase f VName)
onDim (Var (QualName [VName]
_ VName
v) f StructType
typ SrcLoc
loc)
| Just SizeBinder VName
size <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
== VName
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes = do
Maybe VName
prev <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v
case Maybe VName
prev of
Maybe VName
Nothing -> do
VName
v' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
v
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Constraint -> TermTypeM ()
constrain VName
v' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (ExpBase Info VName) -> Usage -> Constraint
Size forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$
forall a. Located a => a -> Text -> Usage
mkUsage SizeBinder VName
size Text
"ambiguous size of bound expression"
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((VName
v, VName
v') :)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var (forall v. v -> QualName v
qualName VName
v') f StructType
typ SrcLoc
loc
Just VName
v' ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var (forall v. v -> QualName v
qualName VName
v') f StructType
typ SrcLoc
loc
onDim ExpBase f VName
d = forall (f :: * -> *) a. Applicative f => a -> f a
pure ExpBase f VName
d
binding ::
[Ident StructType] ->
TermTypeM a ->
TermTypeM a
binding :: forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding [Ident StructType]
idents TermTypeM a
m =
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope (TermScope -> [Ident StructType] -> TermScope
`bindVars` [Ident StructType]
idents) forall a b. (a -> b) -> a -> b
$ do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident StructType]
idents forall a b. (a -> b) -> a -> b
$ \Ident StructType
ident ->
VName -> Constraint -> TermTypeM ()
constrain (forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident) forall a b. (a -> b) -> a -> b
$ SrcLoc -> Constraint
ParamSize forall a b. (a -> b) -> a -> b
$ forall a. Located a => a -> SrcLoc
srclocOf Ident StructType
ident
TermTypeM a
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TermTypeM ()
checkIfUsed
where
bindVars :: TermScope -> [Ident StructType] -> TermScope
bindVars = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TermScope -> Ident StructType -> TermScope
bindVar
bindVar :: TermScope -> Ident StructType -> TermScope
bindVar TermScope
scope (Ident VName
name (Info StructType
tp) SrcLoc
_) =
TermScope
scope
{ scopeVtable :: Map VName ValBinding
scopeVtable =
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name ([TypeParam] -> StructType -> ValBinding
BoundV [] StructType
tp) forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope
}
checkIfUsed :: TermTypeM ()
checkIfUsed = do
Set VName
used <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Set VName
stateUsed
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
used) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName) [Ident StructType]
idents) forall a b. (a -> b) -> a -> b
$ \Ident StructType
ident ->
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
"_" Text -> Text -> Bool
`T.isPrefixOf` Name -> Text
nameToText (VName -> Name
baseName (forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident))) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Ident StructType
ident forall a b. (a -> b) -> a -> b
$
Doc ()
"Unused variable "
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName (forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident))
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
bindingTypes ::
[Either (VName, TypeBinding) (VName, Constraint)] ->
TermTypeM a ->
TermTypeM a
bindingTypes :: forall a.
[Either (VName, TypeBinding) (VName, Constraint)]
-> TermTypeM a -> TermTypeM a
bindingTypes [Either (VName, TypeBinding) (VName, Constraint)]
types TermTypeM a
m = do
Int
lvl <- forall (m :: * -> *). MonadUnify m => m Int
curLevel
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Int
lvl,) (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, Constraint)]
constraints))
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
extend TermTypeM a
m
where
([(VName, TypeBinding)]
tbinds, [(VName, Constraint)]
constraints) = forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (VName, TypeBinding) (VName, Constraint)]
types
extend :: TermScope -> TermScope
extend TermScope
scope =
TermScope
scope
{ scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, TypeBinding)]
tbinds forall a. Semigroup a => a -> a -> a
<> TermScope -> Map VName TypeBinding
scopeTypeTable TermScope
scope
}
bindingTypeParams :: [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams :: forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams [TypeParam]
tparams =
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe (Ident StructType)
typeParamIdent [TypeParam]
tparams)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[Either (VName, TypeBinding) (VName, Constraint)]
-> TermTypeM a -> TermTypeM a
bindingTypes (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)]
typeParamType [TypeParam]
tparams)
where
typeParamType :: TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)]
typeParamType (TypeParamType Liftedness
l VName
v SrcLoc
loc) =
[ forall a b. a -> Either a b
Left (VName
v, Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar forall a. Monoid a => a
mempty (forall v. v -> QualName v
qualName VName
v) [])),
forall a b. b -> Either a b
Right (VName
v, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc)
]
typeParamType (TypeParamDim VName
v SrcLoc
loc) =
[forall a b. b -> Either a b
Right (VName
v, SrcLoc -> Constraint
ParamSize SrcLoc
loc)]
typeParamIdent :: TypeParam -> Maybe (Ident StructType)
typeParamIdent :: TypeParam -> Maybe (Ident StructType)
typeParamIdent (TypeParamDim VName
v SrcLoc
loc) =
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident VName
v (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) SrcLoc
loc
typeParamIdent TypeParam
_ = forall a. Maybe a
Nothing
bindingIdent ::
IdentBase NoInfo Name StructType ->
StructType ->
(Ident StructType -> TermTypeM a) ->
TermTypeM a
bindingIdent :: forall a.
IdentBase NoInfo Name StructType
-> StructType -> (Ident StructType -> TermTypeM a) -> TermTypeM a
bindingIdent (Ident Name
v NoInfo StructType
NoInfo SrcLoc
vloc) StructType
t Ident StructType -> TermTypeM a
m =
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
v)] forall a b. (a -> b) -> a -> b
$ do
VName
v' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
vloc
let ident :: Ident StructType
ident = forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident VName
v' (forall a. a -> Info a
Info StructType
t) SrcLoc
vloc
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding [Ident StructType
ident] forall a b. (a -> b) -> a -> b
$ Ident StructType -> TermTypeM a
m Ident StructType
ident
bindingSizes :: [SizeBinder Name] -> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes :: forall a.
[SizeBinder Name]
-> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes [] [SizeBinder VName] -> TermTypeM a
m = [SizeBinder VName] -> TermTypeM a
m []
bindingSizes [SizeBinder Name]
sizes [SizeBinder VName] -> TermTypeM a
m = do
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ forall {k} {m :: * -> *}.
(Ord k, MonadTypeChecker m) =>
Map k SrcLoc -> SizeBinder k -> m (Map k SrcLoc)
lookForDuplicates forall a. Monoid a => a
mempty [SizeBinder Name]
sizes
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. SizeBinder b -> (Namespace, b)
sizeWithSpace [SizeBinder Name]
sizes) forall a b. (a -> b) -> a -> b
$ do
[SizeBinder VName]
sizes' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {f :: * -> *}.
MonadTypeChecker f =>
SizeBinder Name -> f (SizeBinder VName)
check [SizeBinder Name]
sizes
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (forall a b. (a -> b) -> [a] -> [b]
map forall {vn} {dim} {u}.
SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
sizeWithType [SizeBinder VName]
sizes') forall a b. (a -> b) -> a -> b
$ [SizeBinder VName] -> TermTypeM a
m [SizeBinder VName]
sizes'
where
lookForDuplicates :: Map k SrcLoc -> SizeBinder k -> m (Map k SrcLoc)
lookForDuplicates Map k SrcLoc
prev SizeBinder k
size
| Just SrcLoc
prevloc <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) Map k SrcLoc
prev =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder k
size forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Size name also bound at "
forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty (forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel (forall a. Located a => a -> SrcLoc
srclocOf SizeBinder k
size) SrcLoc
prevloc)
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
| Bool
otherwise =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) (forall a. Located a => a -> SrcLoc
srclocOf SizeBinder k
size) Map k SrcLoc
prev
sizeWithSpace :: SizeBinder b -> (Namespace, b)
sizeWithSpace SizeBinder b
size =
(Namespace
Term, forall vn. SizeBinder vn -> vn
sizeName SizeBinder b
size)
sizeWithType :: SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
sizeWithType SizeBinder vn
size =
forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident (forall vn. SizeBinder vn -> vn
sizeName SizeBinder vn
size) (forall a. a -> Info a
Info (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. PrimType -> ScalarTypeBase dim u
Prim (IntType -> PrimType
Signed IntType
Int64)))) (forall a. Located a => a -> SrcLoc
srclocOf SizeBinder vn
size)
check :: SizeBinder Name -> f (SizeBinder VName)
check (SizeBinder Name
v SrcLoc
loc) =
forall vn. vn -> SrcLoc -> SizeBinder vn
SizeBinder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
loc forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam (SizeBinder VName
v SrcLoc
loc) = forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim (VName -> Name
baseName VName
v) SrcLoc
loc
patLitMkType :: PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType :: PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType (PatLitInt Integer
_) SrcLoc
loc = do
ParamType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyNumberType (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"integer literal") (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ParamType
t
patLitMkType (PatLitFloat Double
_) SrcLoc
loc = do
ParamType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyFloatType (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"float literal") (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ParamType
t
patLitMkType (PatLitPrim PrimValue
v) SrcLoc
_ =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar forall a b. (a -> b) -> a -> b
$ forall dim u. PrimType -> ScalarTypeBase dim u
Prim forall a b. (a -> b) -> a -> b
$ PrimValue -> PrimType
primValueType PrimValue
v
checkPat' ::
[SizeBinder VName] ->
UncheckedPat ParamType ->
Inferred ParamType ->
TermTypeM (Pat ParamType)
checkPat' :: [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes (PatParens PatBase NoInfo Name ParamType
p SrcLoc
loc) Inferred ParamType
t =
forall (f :: * -> *) vn t.
PatBase f vn t -> SrcLoc -> PatBase f vn t
PatParens forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p Inferred ParamType
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatAttr AttrInfo Name
attr PatBase NoInfo Name ParamType
p SrcLoc
loc) Inferred ParamType
t =
forall (f :: * -> *) vn t.
AttrInfo vn -> PatBase f vn t -> SrcLoc -> PatBase f vn t
PatAttr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr AttrInfo Name
attr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p Inferred ParamType
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo ParamType
_ SrcLoc
loc) Inferred ParamType
_
| Name
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
doNotShadow =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ Doc ()
"The" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Name
name forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"operator may not be redefined."
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo ParamType
NoInfo SrcLoc
loc) (Ascribed ParamType
t) = do
VName
name' <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
Id VName
name' (forall a. a -> Info a
Info ParamType
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo ParamType
NoInfo SrcLoc
loc) Inferred ParamType
NoneInferred = do
VName
name' <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
ParamType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
Id VName
name' (forall a. a -> Info a
Info ParamType
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Wildcard NoInfo ParamType
_ SrcLoc
loc) (Ascribed ParamType
t) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
Wildcard (forall a. a -> Info a
Info ParamType
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Wildcard NoInfo ParamType
NoInfo SrcLoc
loc) Inferred ParamType
NoneInferred = do
ParamType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
Wildcard (forall a. a -> Info a
Info ParamType
t) SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (TuplePat [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) (Ascribed ParamType
t)
| Just [ParamType]
ts <- forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord ParamType
t,
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps =
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes) [PatBase NoInfo Name ParamType]
ps (forall a b. (a -> b) -> [a] -> [b]
map forall t. t -> Inferred t
Ascribed [ParamType]
ts)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes p :: PatBase NoInfo Name ParamType
p@(TuplePat [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) (Ascribed ParamType
t) = do
[StructType]
ps_t <- forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps) (forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t")
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching a tuple pattern") (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [StructType]
ps_t)) (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
ParamType
t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully ParamType
t
[SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall a b. (a -> b) -> a -> b
$ forall t. t -> Inferred t
Ascribed ParamType
t'
checkPat' [SizeBinder VName]
sizes (TuplePat [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) Inferred ParamType
NoneInferred =
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PatBase NoInfo Name ParamType
p -> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall t. Inferred t
NoneInferred) [PatBase NoInfo Name ParamType]
ps forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (RecordPat [(Name, PatBase NoInfo Name ParamType)]
p_fs SrcLoc
_) Inferred ParamType
_
| Just (Name
f, PatBase NoInfo Name ParamType
fp) <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
"_" `isPrefixOf`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, PatBase NoInfo Name ParamType)]
p_fs =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError PatBase NoInfo Name ParamType
fp forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Underscore-prefixed fields are not allowed."
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Did you mean" forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Int -> [a] -> [a]
drop Int
1 (Name -> [Char]
nameToString Name
f)) forall a. Semigroup a => a -> a -> a
<> Doc ()
"=_") forall a. Semigroup a => a -> a -> a
<> Doc ()
"?"
checkPat' [SizeBinder VName]
sizes (RecordPat [(Name, PatBase NoInfo Name ParamType)]
p_fs SrcLoc
loc) (Ascribed (Scalar (Record Map Name ParamType
t_fs)))
| forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name ParamType)]
p_fs) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name ParamType
t_fs) =
forall (f :: * -> *) vn t.
[(Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermTypeM (Map Name (Pat ParamType))
check forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
where
check :: TermTypeM (Map Name (Pat ParamType))
check =
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes)) forall a b. (a -> b) -> a -> b
$
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
p_fs) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. t -> Inferred t
Ascribed Map Name ParamType
t_fs)
checkPat' [SizeBinder VName]
sizes p :: PatBase NoInfo Name ParamType
p@(RecordPat [(Name, PatBase NoInfo Name ParamType)]
fields SrcLoc
loc) (Ascribed ParamType
t) = do
Map Name StructType
fields' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t") forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
fields
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name StructType
fields') forall a. Eq a => a -> a -> Bool
/= forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name ParamType)]
fields)) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Duplicate fields in record pattern" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty PatBase NoInfo Name ParamType
p forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching a record pattern") (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record Map Name StructType
fields')) (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
ParamType
t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully ParamType
t
[SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall a b. (a -> b) -> a -> b
$ forall t. t -> Inferred t
Ascribed ParamType
t'
checkPat' [SizeBinder VName]
sizes (RecordPat [(Name, PatBase NoInfo Name ParamType)]
fs SrcLoc
loc) Inferred ParamType
NoneInferred =
forall (f :: * -> *) vn t.
[(Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\PatBase NoInfo Name ParamType
p -> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall t. Inferred t
NoneInferred) (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
fs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatAscription PatBase NoInfo Name ParamType
p TypeExp NoInfo Name
t SrcLoc
loc) Inferred ParamType
maybe_outer_t = do
(TypeExp Info VName
t', ResType
st, [VName]
_) <- TypeExp NoInfo Name
-> TermTypeM (TypeExp Info VName, ResType, [VName])
checkTypeExpNonrigid TypeExp NoInfo Name
t
case Inferred ParamType
maybe_outer_t of
Ascribed ParamType
outer_t -> do
StructType
st_forunify <- [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor [SizeBinder VName]
sizes forall a b. (a -> b) -> a -> b
$ forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ResType
st
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"explicit type ascription") StructType
st_forunify (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
outer_t)
forall (f :: * -> *) vn t.
PatBase f vn t -> TypeExp f vn -> SrcLoc -> PatBase f vn t
PatAscription
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p (forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Info VName
t'
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
Inferred ParamType
NoneInferred ->
forall (f :: * -> *) vn t.
PatBase f vn t -> TypeExp f vn -> SrcLoc -> PatBase f vn t
PatAscription
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p (forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Info VName
t'
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (PatLit PatLit
l NoInfo ParamType
NoInfo SrcLoc
loc) (Ascribed ParamType
t) = do
ParamType
t' <- PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType PatLit
l SrcLoc
loc
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching against literal") (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t') (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t.
PatLit -> f t -> SrcLoc -> PatBase f vn t
PatLit PatLit
l (forall a. a -> Info a
Info ParamType
t') SrcLoc
loc
checkPat' [SizeBinder VName]
_ (PatLit PatLit
l NoInfo ParamType
NoInfo SrcLoc
loc) Inferred ParamType
NoneInferred = do
ParamType
t' <- PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType PatLit
l SrcLoc
loc
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t.
PatLit -> f t -> SrcLoc -> PatBase f vn t
PatLit PatLit
l (forall a. a -> Info a
Info ParamType
t') SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) (Ascribed (Scalar (Sum Map Name [ParamType]
cs)))
| Just [ParamType]
ts <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name [ParamType]
cs = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Pattern #" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Name
n forall a. Semigroup a => a -> a -> a
<> Doc ()
" expects"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"constructor arguments, but type provides"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arguments."
[Pat ParamType]
ps' <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes) [PatBase NoInfo Name ParamType]
ps forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. t -> Inferred t
Ascribed [ParamType]
ts
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (forall a. a -> Info a
Info (forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
Sum Map Name [ParamType]
cs))) [Pat ParamType]
ps' SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) (Ascribed ParamType
t) = do
StructType
t' <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
[Pat ParamType]
ps' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [PatBase NoInfo Name ParamType]
ps forall a b. (a -> b) -> a -> b
$ \PatBase NoInfo Name ParamType
p -> do
ParamType
p_t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (forall a. Located a => a -> SrcLoc
srclocOf PatBase NoInfo Name ParamType
p) Name
"t"
[SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall a b. (a -> b) -> a -> b
$ forall t. t -> Inferred t
Ascribed ParamType
p_t
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct StructType
t') (forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat ParamType]
ps')
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t' (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
ParamType
t'' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully ParamType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (forall a. a -> Info a
Info ParamType
t'') [Pat ParamType]
ps' SrcLoc
loc
where
usage :: Usage
usage = forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching against constructor"
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) Inferred ParamType
NoneInferred = do
[Pat ParamType]
ps' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PatBase NoInfo Name ParamType
p -> [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name ParamType
p forall t. Inferred t
NoneInferred) [PatBase NoInfo Name ParamType]
ps
ParamType
t <- forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n (forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t) (forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat ParamType]
ps')
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (forall a. a -> Info a
Info ParamType
t) [Pat ParamType]
ps' SrcLoc
loc
where
usage :: Usage
usage = forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching against constructor"
checkPat ::
[SizeBinder VName] ->
UncheckedPat (TypeBase Size u) ->
Inferred StructType ->
(Pat ParamType -> TermTypeM a) ->
TermTypeM a
checkPat :: forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [SizeBinder VName]
sizes UncheckedPat (TypeBase (ExpBase Info VName) u)
p Inferred StructType
t Pat ParamType -> TermTypeM a
m = do
forall (m :: * -> *) t.
MonadTypeChecker m =>
[UncheckedTypeParam] -> [UncheckedPat t] -> m ()
checkForDuplicateNames (forall a b. (a -> b) -> [a] -> [b]
map SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam [SizeBinder VName]
sizes) [UncheckedPat (TypeBase (ExpBase Info VName) u)
p]
Pat ParamType
p' <-
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (UncheckedPat StructType -> Inferred StructType -> Checking
CheckingPat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct UncheckedPat (TypeBase (ExpBase Info VName) u)
p) Inferred StructType
t) forall a b. (a -> b) -> a -> b
$
[SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe) UncheckedPat (TypeBase (ExpBase Info VName) u)
p) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe) Inferred StructType
t)
let explicit :: Set VName
explicit = StructType -> Set VName
mustBeExplicitInType forall a b. (a -> b) -> a -> b
$ forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType Pat ParamType
p'
case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
explicit) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes of
SizeBinder VName
size : [SizeBinder VName]
_ ->
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder VName
size forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot bind"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SizeBinder VName
size
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as it is never used as the size of a concrete (non-function) value."
[] ->
forall (m :: * -> *) a. MonadTypeChecker m => NameMap -> m a -> m a
bindNameMap (forall t. Pat t -> NameMap
patNameMap Pat ParamType
p') forall a b. (a -> b) -> a -> b
$ Pat ParamType -> TermTypeM a
m Pat ParamType
p'
bindingPat ::
[SizeBinder VName] ->
UncheckedPat (TypeBase Size u) ->
StructType ->
(Pat ParamType -> TermTypeM a) ->
TermTypeM a
bindingPat :: forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes UncheckedPat (TypeBase (ExpBase Info VName) u)
p StructType
t Pat ParamType -> TermTypeM a
m = do
forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [SizeBinder VName]
sizes UncheckedPat (TypeBase (ExpBase Info VName) u)
p (forall t. t -> Inferred t
Ascribed StructType
t) forall a b. (a -> b) -> a -> b
$ \Pat ParamType
p' -> forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (forall t. Pat t -> [Ident t]
patIdents (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p')) forall a b. (a -> b) -> a -> b
$
case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.notMember` FV -> Set VName
fvVars (forall u. Pat (TypeBase (ExpBase Info VName) u) -> FV
freeInPat Pat ParamType
p')) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes of
[] -> Pat ParamType -> TermTypeM a
m Pat ParamType
p'
SizeBinder VName
size : [SizeBinder VName]
_ -> forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
size
patNameMap :: Pat t -> NameMap
patNameMap :: forall t. Pat t -> NameMap
patNameMap = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map VName -> ((Namespace, Name), QualName VName)
asTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Pat t -> [VName]
patNames
where
asTerm :: VName -> ((Namespace, Name), QualName VName)
asTerm VName
v = ((Namespace
Term, VName -> Name
baseName VName
v), forall v. v -> QualName v
qualName VName
v)
bindingParams ::
[UncheckedTypeParam] ->
[UncheckedPat ParamType] ->
([TypeParam] -> [Pat ParamType] -> TermTypeM a) ->
TermTypeM a
bindingParams :: forall a.
[UncheckedTypeParam]
-> [PatBase NoInfo Name ParamType]
-> ([TypeParam] -> [Pat ParamType] -> TermTypeM a)
-> TermTypeM a
bindingParams [UncheckedTypeParam]
tps [PatBase NoInfo Name ParamType]
orig_ps [TypeParam] -> [Pat ParamType] -> TermTypeM a
m = do
forall (m :: * -> *) t.
MonadTypeChecker m =>
[UncheckedTypeParam] -> [UncheckedPat t] -> m ()
checkForDuplicateNames [UncheckedTypeParam]
tps [PatBase NoInfo Name ParamType]
orig_ps
forall (m :: * -> *) a.
MonadTypeChecker m =>
[UncheckedTypeParam] -> ([TypeParam] -> m a) -> m a
checkTypeParams [UncheckedTypeParam]
tps forall a b. (a -> b) -> a -> b
$ \[TypeParam]
tps' -> forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams [TypeParam]
tps' forall a b. (a -> b) -> a -> b
$ do
let descend :: [Pat ParamType]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM a
descend [Pat ParamType]
ps' (UncheckedPat (TypeBase (ExpBase Info VName) u)
p : [UncheckedPat (TypeBase (ExpBase Info VName) u)]
ps) =
forall u a.
[SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [] UncheckedPat (TypeBase (ExpBase Info VName) u)
p forall t. Inferred t
NoneInferred forall a b. (a -> b) -> a -> b
$ \Pat ParamType
p' ->
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (forall t. Pat t -> [Ident t]
patIdents forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p') forall a b. (a -> b) -> a -> b
$ [Pat ParamType]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM a
descend (Pat ParamType
p' forall a. a -> [a] -> [a]
: [Pat ParamType]
ps') [UncheckedPat (TypeBase (ExpBase Info VName) u)]
ps
descend [Pat ParamType]
ps' [] = [TypeParam] -> [Pat ParamType] -> TermTypeM a
m [TypeParam]
tps' forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Pat ParamType]
ps'
forall {u}.
[Pat ParamType]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM a
descend [] [PatBase NoInfo Name ParamType]
orig_ps