-- | Type checking of patterns.
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)

-- | Names that may not be shadowed.
doNotShadow :: [Name]
doNotShadow :: [Name]
doNotShadow = [Name
"&&", Name
"||"]

nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor [] StructType
t = StructType -> TermTypeM StructType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t -- Minor optimisation.
nonrigidFor [SizeBinder VName]
sizes StructType
t = StateT [(VName, VName)] TermTypeM StructType
-> [(VName, VName)] -> TermTypeM StructType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((ExpBase Info VName
 -> StateT [(VName, VName)] TermTypeM (ExpBase Info VName))
-> (NoUniqueness -> StateT [(VName, VName)] TermTypeM NoUniqueness)
-> StructType
-> StateT [(VName, VName)] TermTypeM StructType
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> TypeBase a b -> f (TypeBase c d)
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 ExpBase Info VName
-> StateT [(VName, VName)] TermTypeM (ExpBase Info VName)
forall {t :: (* -> *) -> * -> *} {f :: * -> *}.
(MonadState [(VName, VName)] (t TermTypeM), MonadTrans t) =>
ExpBase f VName -> t TermTypeM (ExpBase f VName)
onDim NoUniqueness -> StateT [(VName, VName)] TermTypeM NoUniqueness
forall a. a -> StateT [(VName, VName)] TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t) [(VName, VName)]
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 <- (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> Maybe (SizeBinder VName)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
v) (VName -> Bool)
-> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes = do
          Maybe VName
prev <- ([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName))
-> ([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName)
forall a b. (a -> b) -> a -> b
$ VName -> [(VName, VName)] -> Maybe VName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v
          case Maybe VName
prev of
            Maybe VName
Nothing -> do
              VName
v' <- TermTypeM VName -> t TermTypeM VName
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM VName -> t TermTypeM VName)
-> TermTypeM VName -> t TermTypeM VName
forall a b. (a -> b) -> a -> b
$ Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID (Name -> TermTypeM VName) -> Name -> TermTypeM VName
forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
v
              TermTypeM () -> t TermTypeM ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM () -> t TermTypeM ())
-> (Usage -> TermTypeM ()) -> Usage -> t TermTypeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Constraint -> TermTypeM ()
constrain VName
v' (Constraint -> TermTypeM ())
-> (Usage -> Constraint) -> Usage -> TermTypeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (ExpBase Info VName) -> Usage -> Constraint
Size Maybe (ExpBase Info VName)
forall a. Maybe a
Nothing (Usage -> t TermTypeM ()) -> Usage -> t TermTypeM ()
forall a b. (a -> b) -> a -> b
$
                SizeBinder VName -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SizeBinder VName
size Text
"ambiguous size of bound expression"
              ([(VName, VName)] -> [(VName, VName)]) -> t TermTypeM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((VName
v, VName
v') :)
              ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a. a -> t TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpBase f VName -> t TermTypeM (ExpBase f VName))
-> ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a b. (a -> b) -> a -> b
$ QualName VName -> f StructType -> SrcLoc -> ExpBase f VName
forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v') f StructType
typ SrcLoc
loc
            Just VName
v' ->
              ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a. a -> t TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExpBase f VName -> t TermTypeM (ExpBase f VName))
-> ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a b. (a -> b) -> a -> b
$ QualName VName -> f StructType -> SrcLoc -> ExpBase f VName
forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v') f StructType
typ SrcLoc
loc
    onDim ExpBase f VName
d = ExpBase f VName -> t TermTypeM (ExpBase f VName)
forall a. a -> t TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExpBase f VName
d

-- | Bind these identifiers locally while running the provided action.
binding ::
  [Ident StructType] ->
  TermTypeM a ->
  TermTypeM a
binding :: forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding [Ident StructType]
idents TermTypeM a
m =
  (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope (TermScope -> [Ident StructType] -> TermScope
`bindVars` [Ident StructType]
idents) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    -- Those identifiers that can potentially also be sizes are
    -- added as type constraints.  This is necessary so that we
    -- can properly detect scope violations during unification.
    -- We do this for *all* identifiers, not just those that are
    -- integers, because they may become integers later due to
    -- inference...
    [Ident StructType]
-> (Ident StructType -> TermTypeM ()) -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident StructType]
idents ((Ident StructType -> TermTypeM ()) -> TermTypeM ())
-> (Ident StructType -> TermTypeM ()) -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ \Ident StructType
ident ->
      VName -> Constraint -> TermTypeM ()
constrain (Ident StructType -> VName
forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident) (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Constraint
ParamSize (SrcLoc -> Constraint) -> SrcLoc -> Constraint
forall a b. (a -> b) -> a -> b
$ Ident StructType -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Ident StructType
ident
    TermTypeM a
m TermTypeM a -> TermTypeM () -> TermTypeM a
forall a b. TermTypeM a -> TermTypeM b -> TermTypeM a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* TermTypeM ()
checkIfUsed
  where
    bindVars :: TermScope -> [Ident StructType] -> TermScope
bindVars = (TermScope -> Ident StructType -> TermScope)
-> TermScope -> [Ident StructType] -> TermScope
forall b a. (b -> a -> b) -> b -> [a] -> b
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 =
            VName -> ValBinding -> Map VName ValBinding -> Map VName ValBinding
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name ([TypeParam] -> StructType -> ValBinding
BoundV [] StructType
tp) (Map VName ValBinding -> Map VName ValBinding)
-> Map VName ValBinding -> Map VName ValBinding
forall a b. (a -> b) -> a -> b
$ TermScope -> Map VName ValBinding
scopeVtable TermScope
scope
        }

    checkIfUsed :: TermTypeM ()
checkIfUsed = do
      Set VName
used <- (TermTypeState -> Set VName) -> TermTypeM (Set VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TermTypeState -> Set VName
stateUsed
      [Ident StructType]
-> (Ident StructType -> TermTypeM ()) -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Ident StructType -> Bool)
-> [Ident StructType] -> [Ident StructType]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
used) (VName -> Bool)
-> (Ident StructType -> VName) -> Ident StructType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident StructType -> VName
forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName) [Ident StructType]
idents) ((Ident StructType -> TermTypeM ()) -> TermTypeM ())
-> (Ident StructType -> TermTypeM ()) -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ \Ident StructType
ident ->
        Bool -> TermTypeM () -> TermTypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
"_" Text -> Text -> Bool
`T.isPrefixOf` Name -> Text
nameToText (VName -> Name
baseName (Ident StructType -> VName
forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident))) (TermTypeM () -> TermTypeM ()) -> TermTypeM () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
          Ident StructType -> Doc () -> TermTypeM ()
forall loc. Located loc => loc -> Doc () -> TermTypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn Ident StructType
ident (Doc () -> TermTypeM ()) -> Doc () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Unused variable "
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes (VName -> Doc ()
forall a. VName -> Doc a
forall v a. IsName v => v -> Doc a
prettyName (Ident StructType -> VName
forall {k} (f :: k -> *) vn (t :: k). IdentBase f vn t -> vn
identName Ident StructType
ident))
              Doc () -> Doc () -> Doc ()
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 <- TermTypeM Int
forall (m :: * -> *). MonadUnify m => m Int
curLevel
  (Constraints -> Constraints) -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<> (Constraint -> (Int, Constraint))
-> Map VName Constraint -> Constraints
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Int
lvl,) ([(VName, Constraint)] -> Map VName Constraint
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, Constraint)]
constraints))
  (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
extend TermTypeM a
m
  where
    ([(VName, TypeBinding)]
tbinds, [(VName, Constraint)]
constraints) = [Either (VName, TypeBinding) (VName, Constraint)]
-> ([(VName, TypeBinding)], [(VName, Constraint)])
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 = [(VName, TypeBinding)] -> Map VName TypeBinding
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, TypeBinding)]
tbinds Map VName TypeBinding
-> Map VName TypeBinding -> Map VName TypeBinding
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 =
  [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding ((TypeParam -> Maybe (Ident StructType))
-> [TypeParam] -> [Ident StructType]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe (Ident StructType)
typeParamIdent [TypeParam]
tparams)
    (TermTypeM a -> TermTypeM a)
-> (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either (VName, TypeBinding) (VName, Constraint)]
-> TermTypeM a -> TermTypeM a
forall a.
[Either (VName, TypeBinding) (VName, Constraint)]
-> TermTypeM a -> TermTypeM a
bindingTypes ((TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)])
-> [TypeParam] -> [Either (VName, TypeBinding) (VName, Constraint)]
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) =
      [ (VName, TypeBinding)
-> Either (VName, TypeBinding) (VName, Constraint)
forall a b. a -> Either a b
Left (VName
v, Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [] (StructRetType -> TypeBinding) -> StructRetType -> TypeBinding
forall a b. (a -> b) -> a -> b
$ [VName] -> StructType -> StructRetType
forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] (StructType -> StructRetType) -> StructType -> StructRetType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (NoUniqueness
-> QualName VName
-> [TypeArg (ExpBase Info VName)]
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim u.
u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
TypeVar NoUniqueness
forall a. Monoid a => a
mempty (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) [])),
        (VName, Constraint)
-> Either (VName, TypeBinding) (VName, Constraint)
forall a b. b -> Either a b
Right (VName
v, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc)
      ]
    typeParamType (TypeParamDim VName
v SrcLoc
loc) =
      [(VName, Constraint)
-> Either (VName, TypeBinding) (VName, Constraint)
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) =
  Ident StructType -> Maybe (Ident StructType)
forall a. a -> Maybe a
Just (Ident StructType -> Maybe (Ident StructType))
-> Ident StructType -> Maybe (Ident StructType)
forall a b. (a -> b) -> a -> b
$ VName -> Info StructType -> SrcLoc -> Ident StructType
forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident VName
v (StructType -> Info StructType
forall a. a -> Info a
Info (StructType -> Info StructType) -> StructType -> Info StructType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType)
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim u. PrimType -> ScalarTypeBase dim u
Prim (PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness)
-> PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) SrcLoc
loc
typeParamIdent TypeParam
_ = Maybe (Ident StructType)
forall a. Maybe a
Nothing

-- | Bind a single term-level identifier.
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 =
  [(Namespace, Name)] -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
v)] (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    VName
v' <- Namespace -> Name -> SrcLoc -> TermTypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
vloc
    let ident :: Ident StructType
ident = VName -> Info StructType -> SrcLoc -> Ident StructType
forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident VName
v' (StructType -> Info StructType
forall a. a -> Info a
Info StructType
t) SrcLoc
vloc
    [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding [Ident StructType
ident] (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ Ident StructType -> TermTypeM a
m Ident StructType
ident

-- | Bind @let@-bound sizes.  This is usually followed by 'bindingPat'
-- immediately afterwards.
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 [] -- Minor optimisation.
bindingSizes [SizeBinder Name]
sizes [SizeBinder VName] -> TermTypeM a
m = do
  (Map Name SrcLoc -> SizeBinder Name -> TermTypeM (Map Name SrcLoc))
-> Map Name SrcLoc -> [SizeBinder Name] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ Map Name SrcLoc -> SizeBinder Name -> TermTypeM (Map Name SrcLoc)
forall {k} {m :: * -> *}.
(Ord k, MonadTypeChecker m) =>
Map k SrcLoc -> SizeBinder k -> m (Map k SrcLoc)
lookForDuplicates Map Name SrcLoc
forall a. Monoid a => a
mempty [SizeBinder Name]
sizes
  [(Namespace, Name)] -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced ((SizeBinder Name -> (Namespace, Name))
-> [SizeBinder Name] -> [(Namespace, Name)]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder Name -> (Namespace, Name)
forall {b}. SizeBinder b -> (Namespace, b)
sizeWithSpace [SizeBinder Name]
sizes) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    [SizeBinder VName]
sizes' <- (SizeBinder Name -> TermTypeM (SizeBinder VName))
-> [SizeBinder Name] -> TermTypeM [SizeBinder VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SizeBinder Name -> TermTypeM (SizeBinder VName)
forall {f :: * -> *}.
MonadTypeChecker f =>
SizeBinder Name -> f (SizeBinder VName)
check [SizeBinder Name]
sizes
    [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding ((SizeBinder VName -> Ident StructType)
-> [SizeBinder VName] -> [Ident StructType]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder VName -> Ident StructType
forall {vn} {dim} {u}.
SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
sizeWithType [SizeBinder VName]
sizes') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
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 <- k -> Map k SrcLoc -> Maybe SrcLoc
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (SizeBinder k -> k
forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) Map k SrcLoc
prev =
          SizeBinder k -> Notes -> Doc () -> m (Map k SrcLoc)
forall loc a. Located loc => loc -> Notes -> Doc () -> m a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder k
size Notes
forall a. Monoid a => a
mempty (Doc () -> m (Map k SrcLoc)) -> Doc () -> m (Map k SrcLoc)
forall a b. (a -> b) -> a -> b
$
            Doc ()
"Size name also bound at "
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc ()
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SrcLoc -> SrcLoc -> [Char]
forall a b. (Located a, Located b) => a -> b -> [Char]
locStrRel (SizeBinder k -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder k
size) SrcLoc
prevloc)
              Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
      | Bool
otherwise =
          Map k SrcLoc -> m (Map k SrcLoc)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k SrcLoc -> m (Map k SrcLoc))
-> Map k SrcLoc -> m (Map k SrcLoc)
forall a b. (a -> b) -> a -> b
$ k -> SrcLoc -> Map k SrcLoc -> Map k SrcLoc
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (SizeBinder k -> k
forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) (SizeBinder k -> SrcLoc
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, SizeBinder b -> b
forall vn. SizeBinder vn -> vn
sizeName SizeBinder b
size)
    sizeWithType :: SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
sizeWithType SizeBinder vn
size =
      vn
-> Info (TypeBase dim u)
-> SrcLoc
-> IdentBase Info vn (TypeBase dim u)
forall {k} (f :: k -> *) vn (t :: k).
vn -> f t -> SrcLoc -> IdentBase f vn t
Ident (SizeBinder vn -> vn
forall vn. SizeBinder vn -> vn
sizeName SizeBinder vn
size) (TypeBase dim u -> Info (TypeBase dim u)
forall a. a -> Info a
Info (ScalarTypeBase dim u -> TypeBase dim u
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (PrimType -> ScalarTypeBase dim u
forall dim u. PrimType -> ScalarTypeBase dim u
Prim (IntType -> PrimType
Signed IntType
Int64)))) (SizeBinder vn -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder vn
size)

    check :: SizeBinder Name -> f (SizeBinder VName)
check (SizeBinder Name
v SrcLoc
loc) =
      VName -> SrcLoc -> SizeBinder VName
forall vn. vn -> SrcLoc -> SizeBinder vn
SizeBinder (VName -> SrcLoc -> SizeBinder VName)
-> f VName -> f (SrcLoc -> SizeBinder VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Namespace -> Name -> SrcLoc -> f VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
loc f (SrcLoc -> SizeBinder VName) -> f SrcLoc -> f (SizeBinder VName)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> f SrcLoc
forall a. a -> f a
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) = Name -> SrcLoc -> UncheckedTypeParam
forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim (VName -> Name
baseName VName
v) SrcLoc
loc

-- All this complexity is just so we can handle un-suffixed numeric
-- literals in patterns.
patLitMkType :: PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType :: PatLit -> SrcLoc -> TermTypeM ParamType
patLitMkType (PatLitInt Integer
_) SrcLoc
loc = do
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [PrimType] -> Usage -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyNumberType (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"integer literal") (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  ParamType -> TermTypeM ParamType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ParamType
t
patLitMkType (PatLitFloat Double
_) SrcLoc
loc = do
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [PrimType] -> Usage -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyFloatType (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"float literal") (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  ParamType -> TermTypeM ParamType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ParamType
t
patLitMkType (PatLitPrim PrimValue
v) SrcLoc
_ =
  ParamType -> TermTypeM ParamType
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ParamType -> TermTypeM ParamType)
-> ParamType -> TermTypeM ParamType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (ExpBase Info VName) Diet -> ParamType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (ScalarTypeBase (ExpBase Info VName) Diet -> ParamType)
-> ScalarTypeBase (ExpBase Info VName) Diet -> ParamType
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (ExpBase Info VName) Diet
forall dim u. PrimType -> ScalarTypeBase dim u
Prim (PrimType -> ScalarTypeBase (ExpBase Info VName) Diet)
-> PrimType -> ScalarTypeBase (ExpBase Info VName) Diet
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 =
  Pat ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatBase f vn t -> SrcLoc -> PatBase f vn t
PatParens (Pat ParamType -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType) -> TermTypeM (SrcLoc -> Pat ParamType)
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 TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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 =
  AttrInfo VName -> Pat ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
AttrInfo vn -> PatBase f vn t -> SrcLoc -> PatBase f vn t
PatAttr (AttrInfo VName -> Pat ParamType -> SrcLoc -> Pat ParamType)
-> TermTypeM (AttrInfo VName)
-> TermTypeM (Pat ParamType -> SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrInfo Name -> TermTypeM (AttrInfo VName)
forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr AttrInfo Name
attr TermTypeM (Pat ParamType -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType) -> TermTypeM (SrcLoc -> Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
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 TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
doNotShadow =
      SrcLoc -> Notes -> Doc () -> TermTypeM (Pat ParamType)
forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TermTypeM (Pat ParamType))
-> Doc () -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Doc ()
"The" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
name Doc () -> Doc () -> Doc ()
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' <- Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ VName -> Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
Id VName
name' (ParamType -> Info ParamType
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' <- Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ VName -> Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
Id VName
name' (ParamType -> Info ParamType
forall a. a -> Info a
Info ParamType
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Wildcard NoInfo ParamType
_ SrcLoc
loc) (Ascribed ParamType
t) =
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
Wildcard (ParamType -> Info ParamType
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 <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
Wildcard (ParamType -> Info ParamType
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 <- ParamType -> Maybe [ParamType]
forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord ParamType
t,
    [ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [PatBase NoInfo Name ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps =
      [Pat ParamType] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat
        ([Pat ParamType] -> SrcLoc -> Pat ParamType)
-> TermTypeM [Pat ParamType] -> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name ParamType
 -> Inferred ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo Name ParamType]
-> [Inferred ParamType]
-> TermTypeM [Pat ParamType]
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 ((ParamType -> Inferred ParamType)
-> [ParamType] -> [Inferred ParamType]
forall a b. (a -> b) -> [a] -> [b]
map ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed [ParamType]
ts)
        TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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 <- Int -> TermTypeM StructType -> TermTypeM [StructType]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([PatBase NoInfo Name ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps) (SrcLoc -> Name -> TermTypeM StructType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t")
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching a tuple pattern") (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar ([StructType] -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [StructType]
ps_t)) (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  ParamType
t' <- ParamType -> TermTypeM ParamType
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 (Inferred ParamType -> TermTypeM (Pat ParamType))
-> Inferred ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed ParamType
t'
checkPat' [SizeBinder VName]
sizes (TuplePat [PatBase NoInfo Name ParamType]
ps SrcLoc
loc) Inferred ParamType
NoneInferred =
  [Pat ParamType] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat ([Pat ParamType] -> SrcLoc -> Pat ParamType)
-> TermTypeM [Pat ParamType] -> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo Name ParamType] -> TermTypeM [Pat ParamType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\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 Inferred ParamType
forall t. Inferred t
NoneInferred) [PatBase NoInfo Name ParamType]
ps TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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) <- ((Name, PatBase NoInfo Name ParamType) -> Bool)
-> [(Name, PatBase NoInfo Name ParamType)]
-> Maybe (Name, PatBase NoInfo Name ParamType)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
"_" `isPrefixOf`) ([Char] -> Bool)
-> ((Name, PatBase NoInfo Name ParamType) -> [Char])
-> (Name, PatBase NoInfo Name ParamType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameToString (Name -> [Char])
-> ((Name, PatBase NoInfo Name ParamType) -> Name)
-> (Name, PatBase NoInfo Name ParamType)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, PatBase NoInfo Name ParamType) -> Name
forall a b. (a, b) -> a
fst) [(Name, PatBase NoInfo Name ParamType)]
p_fs =
      PatBase NoInfo Name ParamType
-> Notes -> Doc () -> TermTypeM (Pat ParamType)
forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError PatBase NoInfo Name ParamType
fp Notes
forall a. Monoid a => a
mempty (Doc () -> TermTypeM (Pat ParamType))
-> Doc () -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Underscore-prefixed fields are not allowed."
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"Did you mean"
          Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
dquotes ([Char] -> Doc ()
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
1 (Name -> [Char]
nameToString Name
f)) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"=_")
          Doc () -> Doc () -> 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)))
  | [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (((Name, PatBase NoInfo Name ParamType) -> Name)
-> [(Name, PatBase NoInfo Name ParamType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase NoInfo Name ParamType) -> Name
forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name ParamType)]
p_fs) [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (Map Name ParamType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name ParamType
t_fs) =
      [(Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[(Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
-> (Map Name (Pat ParamType) -> [(Name, Pat ParamType)])
-> Map Name (Pat ParamType)
-> SrcLoc
-> Pat ParamType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (Pat ParamType) -> [(Name, Pat ParamType)]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name (Pat ParamType) -> SrcLoc -> Pat ParamType)
-> TermTypeM (Map Name (Pat ParamType))
-> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermTypeM (Map Name (Pat ParamType))
check TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
  where
    check :: TermTypeM (Map Name (Pat ParamType))
check =
      ((PatBase NoInfo Name ParamType, Inferred ParamType)
 -> TermTypeM (Pat ParamType))
-> Map Name (PatBase NoInfo Name ParamType, Inferred ParamType)
-> TermTypeM (Map Name (Pat ParamType))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse ((PatBase NoInfo Name ParamType
 -> Inferred ParamType -> TermTypeM (Pat ParamType))
-> (PatBase NoInfo Name ParamType, Inferred ParamType)
-> TermTypeM (Pat ParamType)
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)) (Map Name (PatBase NoInfo Name ParamType, Inferred ParamType)
 -> TermTypeM (Map Name (Pat ParamType)))
-> Map Name (PatBase NoInfo Name ParamType, Inferred ParamType)
-> TermTypeM (Map Name (Pat ParamType))
forall a b. (a -> b) -> a -> b
$
        (PatBase NoInfo Name ParamType
 -> Inferred ParamType
 -> (PatBase NoInfo Name ParamType, Inferred ParamType))
-> Map Name (PatBase NoInfo Name ParamType)
-> Map Name (Inferred ParamType)
-> Map Name (PatBase NoInfo Name ParamType, Inferred ParamType)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) ([(Name, PatBase NoInfo Name ParamType)]
-> Map Name (PatBase NoInfo Name ParamType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
p_fs) ((ParamType -> Inferred ParamType)
-> Map Name ParamType -> Map Name (Inferred ParamType)
forall a b. (a -> b) -> Map Name a -> Map Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParamType -> Inferred ParamType
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' <- (PatBase NoInfo Name ParamType -> TermTypeM StructType)
-> Map Name (PatBase NoInfo Name ParamType)
-> TermTypeM (Map Name StructType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name b)
traverse (TermTypeM StructType
-> PatBase NoInfo Name ParamType -> TermTypeM StructType
forall a b. a -> b -> a
const (TermTypeM StructType
 -> PatBase NoInfo Name ParamType -> TermTypeM StructType)
-> TermTypeM StructType
-> PatBase NoInfo Name ParamType
-> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Name -> TermTypeM StructType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t") (Map Name (PatBase NoInfo Name ParamType)
 -> TermTypeM (Map Name StructType))
-> Map Name (PatBase NoInfo Name ParamType)
-> TermTypeM (Map Name StructType)
forall a b. (a -> b) -> a -> b
$ [(Name, PatBase NoInfo Name ParamType)]
-> Map Name (PatBase NoInfo Name ParamType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
fields

  Bool -> TermTypeM () -> TermTypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fields') [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (((Name, PatBase NoInfo Name ParamType) -> Name)
-> [(Name, PatBase NoInfo Name ParamType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase NoInfo Name ParamType) -> Name
forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name ParamType)]
fields)) (TermTypeM () -> TermTypeM ()) -> TermTypeM () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc () -> TermTypeM ()
forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TermTypeM ()) -> Doc () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
      Doc ()
"Duplicate fields in record pattern" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> PatBase NoInfo Name ParamType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PatBase NoInfo Name ParamType -> Doc ann
pretty PatBase NoInfo Name ParamType
p Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching a record pattern") (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (Map Name StructType
-> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
Record Map Name StructType
fields')) (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  ParamType
t' <- ParamType -> TermTypeM ParamType
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 (Inferred ParamType -> TermTypeM (Pat ParamType))
-> Inferred ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed ParamType
t'
checkPat' [SizeBinder VName]
sizes (RecordPat [(Name, PatBase NoInfo Name ParamType)]
fs SrcLoc
loc) Inferred ParamType
NoneInferred =
  [(Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[(Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
-> (Map Name (Pat ParamType) -> [(Name, Pat ParamType)])
-> Map Name (Pat ParamType)
-> SrcLoc
-> Pat ParamType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (Pat ParamType) -> [(Name, Pat ParamType)]
forall k a. Map k a -> [(k, a)]
M.toList
    (Map Name (Pat ParamType) -> SrcLoc -> Pat ParamType)
-> TermTypeM (Map Name (Pat ParamType))
-> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
-> Map Name (PatBase NoInfo Name ParamType)
-> TermTypeM (Map Name (Pat ParamType))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Name a -> f (Map Name 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 Inferred ParamType
forall t. Inferred t
NoneInferred) ([(Name, PatBase NoInfo Name ParamType)]
-> Map Name (PatBase NoInfo Name ParamType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name ParamType)]
fs)
    TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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 (StructType -> TermTypeM StructType)
-> StructType -> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ ResType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ResType
st
      Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"explicit type ascription") StructType
st_forunify (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
outer_t)

      Pat ParamType -> TypeExp Info VName -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatBase f vn t -> TypeExp f vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat ParamType -> TypeExp Info VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType)
-> TermTypeM (TypeExp Info VName -> SrcLoc -> Pat ParamType)
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 (ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
        TermTypeM (TypeExp Info VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (TypeExp Info VName)
-> TermTypeM (SrcLoc -> Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp Info VName -> TermTypeM (TypeExp Info VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Info VName
t'
        TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
    Inferred ParamType
NoneInferred ->
      Pat ParamType -> TypeExp Info VName -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatBase f vn t -> TypeExp f vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat ParamType -> TypeExp Info VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType)
-> TermTypeM (TypeExp Info VName -> SrcLoc -> Pat ParamType)
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 (ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
        TermTypeM (TypeExp Info VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (TypeExp Info VName)
-> TermTypeM (SrcLoc -> Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp Info VName -> TermTypeM (TypeExp Info VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Info VName
t'
        TermTypeM (SrcLoc -> Pat ParamType)
-> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall a. a -> TermTypeM a
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
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SrcLoc
loc Text
"matching against literal") (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t') (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ PatLit -> Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatLit -> f t -> SrcLoc -> PatBase f vn t
PatLit PatLit
l (ParamType -> Info ParamType
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
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ PatLit -> Info ParamType -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatLit -> f t -> SrcLoc -> PatBase f vn t
PatLit PatLit
l (ParamType -> Info ParamType
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 <- Name -> Map Name [ParamType] -> Maybe [ParamType]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name [ParamType]
cs = do
      Bool -> TermTypeM () -> TermTypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([PatBase NoInfo Name ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts) (TermTypeM () -> TermTypeM ()) -> TermTypeM () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
        SrcLoc -> Notes -> Doc () -> TermTypeM ()
forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc () -> TermTypeM ()) -> Doc () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
          Doc ()
"Pattern #" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Name -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. Name -> Doc ann
pretty Name
n Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
" expects"
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ()
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([PatBase NoInfo Name ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo Name ParamType]
ps)
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"constructor arguments, but type provides"
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ()
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ParamType]
ts)
            Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arguments."
      [Pat ParamType]
ps' <- (PatBase NoInfo Name ParamType
 -> Inferred ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo Name ParamType]
-> [Inferred ParamType]
-> TermTypeM [Pat ParamType]
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 ([Inferred ParamType] -> TermTypeM [Pat ParamType])
-> [Inferred ParamType] -> TermTypeM [Pat ParamType]
forall a b. (a -> b) -> a -> b
$ (ParamType -> Inferred ParamType)
-> [ParamType] -> [Inferred ParamType]
forall a b. (a -> b) -> [a] -> [b]
map ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed [ParamType]
ts
      Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Name
-> Info ParamType -> [Pat ParamType] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (ParamType -> Info ParamType
forall a. a -> Info a
Info (ScalarTypeBase (ExpBase Info VName) Diet -> ParamType
forall dim u. ScalarTypeBase dim u -> TypeBase dim u
Scalar (Map Name [ParamType] -> ScalarTypeBase (ExpBase Info VName) Diet
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' <- SrcLoc -> Name -> TermTypeM StructType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [Pat ParamType]
ps' <- [PatBase NoInfo Name ParamType]
-> (PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
-> TermTypeM [Pat ParamType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [PatBase NoInfo Name ParamType]
ps ((PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
 -> TermTypeM [Pat ParamType])
-> (PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
-> TermTypeM [Pat ParamType]
forall a b. (a -> b) -> a -> b
$ \PatBase NoInfo Name ParamType
p -> do
    ParamType
p_t <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (PatBase NoInfo Name ParamType -> SrcLoc
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 (Inferred ParamType -> TermTypeM (Pat ParamType))
-> Inferred ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed ParamType
p_t
  Usage -> Name -> StructType -> [StructType] -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n (StructType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct StructType
t') (Pat ParamType -> StructType
forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType (Pat ParamType -> StructType) -> [Pat ParamType] -> [StructType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat ParamType]
ps')
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t' (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
  ParamType
t'' <- ParamType -> TermTypeM ParamType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully ParamType
t
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Name
-> Info ParamType -> [Pat ParamType] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (ParamType -> Info ParamType
forall a. a -> Info a
Info ParamType
t'') [Pat ParamType]
ps' SrcLoc
loc
  where
    usage :: Usage
usage = SrcLoc -> Text -> 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' <- (PatBase NoInfo Name ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo Name ParamType] -> TermTypeM [Pat ParamType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\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 Inferred ParamType
forall t. Inferred t
NoneInferred) [PatBase NoInfo Name ParamType]
ps
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als dim.
Monoid als =>
SrcLoc -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Usage -> Name -> StructType -> [StructType] -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t) (Pat ParamType -> StructType
forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType (Pat ParamType -> StructType) -> [Pat ParamType] -> [StructType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat ParamType]
ps')
  Pat ParamType -> TermTypeM (Pat ParamType)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat ParamType -> TermTypeM (Pat ParamType))
-> Pat ParamType -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$ Name
-> Info ParamType -> [Pat ParamType] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
Name -> f t -> [PatBase f vn t] -> SrcLoc -> PatBase f vn t
PatConstr Name
n (ParamType -> Info ParamType
forall a. a -> Info a
Info ParamType
t) [Pat ParamType]
ps' SrcLoc
loc
  where
    usage :: Usage
usage = SrcLoc -> Text -> 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
  [UncheckedTypeParam]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM ()
forall (m :: * -> *) t.
MonadTypeChecker m =>
[UncheckedTypeParam] -> [UncheckedPat t] -> m ()
checkForDuplicateNames ((SizeBinder VName -> UncheckedTypeParam)
-> [SizeBinder VName] -> [UncheckedTypeParam]
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' <-
    Checking -> TermTypeM (Pat ParamType) -> TermTypeM (Pat ParamType)
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (UncheckedPat StructType -> Inferred StructType -> Checking
CheckingPat ((TypeBase (ExpBase Info VName) u -> StructType)
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> UncheckedPat StructType
forall a b.
(a -> b) -> PatBase NoInfo Name a -> PatBase NoInfo Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeBase (ExpBase Info VName) u -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct UncheckedPat (TypeBase (ExpBase Info VName) u)
p) Inferred StructType
t) (TermTypeM (Pat ParamType) -> TermTypeM (Pat ParamType))
-> TermTypeM (Pat ParamType) -> TermTypeM (Pat ParamType)
forall a b. (a -> b) -> a -> b
$
      [SizeBinder VName]
-> PatBase NoInfo Name ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [SizeBinder VName]
sizes ((TypeBase (ExpBase Info VName) u -> ParamType)
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> PatBase NoInfo Name ParamType
forall a b.
(a -> b) -> PatBase NoInfo Name a -> PatBase NoInfo Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Diet -> TypeBase (ExpBase Info VName) u -> ParamType
forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe) UncheckedPat (TypeBase (ExpBase Info VName) u)
p) ((StructType -> ParamType)
-> Inferred StructType -> Inferred ParamType
forall a b. (a -> b) -> Inferred a -> Inferred b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Diet -> StructType -> ParamType
forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe) Inferred StructType
t)

  let explicit :: Set VName
explicit = StructType -> Set VName
mustBeExplicitInType (StructType -> Set VName) -> StructType -> Set VName
forall a b. (a -> b) -> a -> b
$ Pat ParamType -> StructType
forall u. Pat (TypeBase (ExpBase Info VName) u) -> StructType
patternStructType Pat ParamType
p'

  case (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> [SizeBinder VName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
explicit) (VName -> Bool)
-> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes of
    SizeBinder VName
size : [SizeBinder VName]
_ ->
      SizeBinder VName -> Notes -> Doc () -> TermTypeM a
forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SizeBinder VName
size Notes
forall a. Monoid a => a
mempty (Doc () -> TermTypeM a) -> Doc () -> TermTypeM a
forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot bind"
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SizeBinder VName -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. SizeBinder VName -> Doc ann
pretty SizeBinder VName
size
          Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as it is never used as the size of a concrete (non-function) value."
    [] ->
      NameMap -> TermTypeM a -> TermTypeM a
forall a. NameMap -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a. MonadTypeChecker m => NameMap -> m a -> m a
bindNameMap (Pat ParamType -> NameMap
forall t. Pat t -> NameMap
patNameMap Pat ParamType
p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ Pat ParamType -> TermTypeM a
m Pat ParamType
p'

-- | Check and bind a @let@-pattern.
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
  [SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
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 (StructType -> Inferred StructType
forall t. t -> Inferred t
Ascribed StructType
t) ((Pat ParamType -> TermTypeM a) -> TermTypeM a)
-> (Pat ParamType -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat ParamType
p' -> [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (Pat StructType -> [Ident StructType]
forall t. Pat t -> [Ident t]
patIdents ((ParamType -> StructType) -> Pat ParamType -> Pat StructType
forall a b.
(a -> b) -> PatBase Info VName a -> PatBase Info VName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p')) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$
    case (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> [SizeBinder VName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` FV -> Set VName
fvVars (Pat ParamType -> FV
forall u. Pat (TypeBase (ExpBase Info VName) u) -> FV
freeInPat Pat ParamType
p')) (VName -> Bool)
-> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes of
      [] -> Pat ParamType -> TermTypeM a
m Pat ParamType
p'
      SizeBinder VName
size : [SizeBinder VName]
_ -> SizeBinder VName -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
size

patNameMap :: Pat t -> NameMap
patNameMap :: forall t. Pat t -> NameMap
patNameMap = [((Namespace, Name), QualName VName)] -> NameMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((Namespace, Name), QualName VName)] -> NameMap)
-> (Pat t -> [((Namespace, Name), QualName VName)])
-> Pat t
-> NameMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> ((Namespace, Name), QualName VName))
-> [VName] -> [((Namespace, Name), QualName VName)]
forall a b. (a -> b) -> [a] -> [b]
map VName -> ((Namespace, Name), QualName VName)
asTerm ([VName] -> [((Namespace, Name), QualName VName)])
-> (Pat t -> [VName])
-> Pat t
-> [((Namespace, Name), QualName VName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat t -> [VName]
forall t. Pat t -> [VName]
patNames
  where
    asTerm :: VName -> ((Namespace, Name), QualName VName)
asTerm VName
v = ((Namespace
Term, VName -> Name
baseName VName
v), VName -> QualName VName
forall v. v -> QualName v
qualName VName
v)

-- | Check and bind type and value parameters.
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
  [UncheckedTypeParam]
-> [PatBase NoInfo Name ParamType] -> TermTypeM ()
forall (m :: * -> *) t.
MonadTypeChecker m =>
[UncheckedTypeParam] -> [UncheckedPat t] -> m ()
checkForDuplicateNames [UncheckedTypeParam]
tps [PatBase NoInfo Name ParamType]
orig_ps
  [UncheckedTypeParam] -> ([TypeParam] -> TermTypeM a) -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[UncheckedTypeParam] -> ([TypeParam] -> m a) -> m a
checkTypeParams [UncheckedTypeParam]
tps (([TypeParam] -> TermTypeM a) -> TermTypeM a)
-> ([TypeParam] -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
tps' -> [TypeParam] -> TermTypeM a -> TermTypeM a
forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams [TypeParam]
tps' (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
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) =
          [SizeBinder VName]
-> UncheckedPat (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
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 Inferred StructType
forall t. Inferred t
NoneInferred ((Pat ParamType -> TermTypeM a) -> TermTypeM a)
-> (Pat ParamType -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat ParamType
p' ->
            [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding (Pat StructType -> [Ident StructType]
forall t. Pat t -> [Ident t]
patIdents (Pat StructType -> [Ident StructType])
-> Pat StructType -> [Ident StructType]
forall a b. (a -> b) -> a -> b
$ (ParamType -> StructType) -> Pat ParamType -> Pat StructType
forall a b.
(a -> b) -> PatBase Info VName a -> PatBase Info VName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct Pat ParamType
p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat ParamType]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM a
descend (Pat ParamType
p' Pat ParamType -> [Pat ParamType] -> [Pat ParamType]
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' ([Pat ParamType] -> TermTypeM a) -> [Pat ParamType] -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat ParamType] -> [Pat ParamType]
forall a. [a] -> [a]
reverse [Pat ParamType]
ps'

    [Pat ParamType] -> [PatBase NoInfo Name ParamType] -> TermTypeM a
forall {u}.
[Pat ParamType]
-> [UncheckedPat (TypeBase (ExpBase Info VName) u)] -> TermTypeM a
descend [] [PatBase NoInfo Name ParamType]
orig_ps