-- | Type checking of patterns.
module Language.Futhark.TypeChecker.Terms.Pat
  ( binding,
    bindingParams,
    bindingPat,
    bindingIdent,
    bindingSizes,
  )
where

import Control.Monad
import Data.Bifunctor
import Data.Either
import Data.List (find, isPrefixOf, sort, sortBy)
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Ord (comparing)
import Data.Set qualified as S
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)

nonrigidFor :: [(SizeBinder VName, QualName VName)] -> StructType -> StructType
nonrigidFor :: [(SizeBinder VName, QualName VName)] -> StructType -> StructType
nonrigidFor [] = StructType -> StructType
forall a. a -> a
id -- Minor optimisation.
nonrigidFor [(SizeBinder VName, QualName VName)]
sizes = (ExpBase Info VName -> ExpBase Info VName)
-> StructType -> StructType
forall a b c. (a -> b) -> TypeBase a c -> TypeBase b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ExpBase Info VName -> ExpBase Info VName
forall {f :: * -> *}. ExpBase f VName -> ExpBase f VName
onDim
  where
    onDim :: ExpBase f VName -> ExpBase f VName
onDim (Var (QualName [VName]
_ VName
v) f StructType
info SrcLoc
loc)
      | Just (SizeBinder VName
_, QualName VName
v') <- ((SizeBinder VName, QualName VName) -> Bool)
-> [(SizeBinder VName, QualName VName)]
-> Maybe (SizeBinder VName, QualName 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, QualName VName) -> VName)
-> (SizeBinder VName, QualName VName)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName (SizeBinder VName -> VName)
-> ((SizeBinder VName, QualName VName) -> SizeBinder VName)
-> (SizeBinder VName, QualName VName)
-> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SizeBinder VName, QualName VName) -> SizeBinder VName
forall a b. (a, b) -> a
fst) [(SizeBinder VName, QualName VName)]
sizes =
          QualName VName -> f StructType -> SrcLoc -> ExpBase f VName
forall (f :: * -> *) vn.
QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
Var QualName VName
v' f StructType
info SrcLoc
loc
    onDim ExpBase f VName
d = 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
$ Loc -> Constraint
ParamSize (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ Ident StructType -> Loc
forall a. Located a => a -> Loc
locOf Ident StructType
ident
    TermTypeM a
m
  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 =
            M.insert name (BoundV [] tp) $ scopeVtable scope
        }

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 = M.fromList tbinds <> scopeTypeTable 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 -> Loc -> Constraint
ParamType Liftedness
l (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc)
      ]
    typeParamType (TypeParamDim VName
v SrcLoc
loc) =
      [(VName, Constraint)
-> Either (VName, TypeBinding) (VName, Constraint)
forall a b. b -> Either a b
Right (VName
v, Loc -> Constraint
ParamSize (Loc -> Constraint) -> Loc -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc)]

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 @let@-bound sizes.  This is usually followed by 'bindingPat'
-- immediately afterwards.
bindingSizes :: [SizeBinder VName] -> TermTypeM a -> TermTypeM a
bindingSizes :: forall a. [SizeBinder VName] -> TermTypeM a -> TermTypeM a
bindingSizes [] TermTypeM a
m = TermTypeM a
m -- Minor optimisation.
bindingSizes [SizeBinder VName]
sizes TermTypeM a
m = [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
m
  where
    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)

-- | Bind a single term-level identifier.
bindingIdent ::
  IdentBase NoInfo VName StructType ->
  StructType ->
  (Ident StructType -> TermTypeM a) ->
  TermTypeM a
bindingIdent :: forall a.
IdentBase NoInfo VName StructType
-> StructType -> (Ident StructType -> TermTypeM a) -> TermTypeM a
bindingIdent (Ident VName
v NoInfo StructType
NoInfo SrcLoc
vloc) StructType
t Ident StructType -> TermTypeM a
m = do
  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

-- 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 a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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 a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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, QualName VName)] ->
  PatBase NoInfo VName ParamType ->
  Inferred ParamType ->
  TermTypeM (Pat ParamType)
checkPat' :: [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes (PatParens PatBase NoInfo VName 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, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName 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, QualName VName)]
sizes (PatAttr AttrInfo VName
attr PatBase NoInfo VName 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 VName -> TermTypeM (AttrInfo VName)
forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo VName -> m (AttrInfo VName)
checkAttr AttrInfo VName
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, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName 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, QualName VName)]
_ (Id VName
name NoInfo ParamType
NoInfo 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
$ 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, QualName VName)]
_ (Id VName
name NoInfo ParamType
NoInfo SrcLoc
loc) Inferred ParamType
NoneInferred = do
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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, QualName 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, QualName VName)]
_ (Wildcard NoInfo ParamType
NoInfo SrcLoc
loc) Inferred ParamType
NoneInferred = do
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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, QualName VName)]
sizes p :: PatBase NoInfo VName ParamType
p@(TuplePat [PatBase NoInfo VName 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 VName ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo VName 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 VName ParamType
 -> Inferred ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo VName ParamType]
-> [Inferred ParamType]
-> TermTypeM [Pat ParamType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes) [PatBase NoInfo VName 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
  | Bool
otherwise = do
      [StructType]
ps_t <- Int -> TermTypeM StructType -> TermTypeM [StructType]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([PatBase NoInfo VName ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo VName ParamType]
ps) (SrcLoc -> Name -> TermTypeM StructType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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)
      [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName 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 -> Inferred ParamType)
-> ParamType -> Inferred ParamType
forall a b. (a -> b) -> a -> b
$ Diet -> StructType -> ParamType
forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe (StructType -> ParamType) -> StructType -> ParamType
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
$ [StructType] -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [StructType]
ps_t
checkPat' [(SizeBinder VName, QualName VName)]
sizes (TuplePat [PatBase NoInfo VName 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 VName ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo VName 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 VName ParamType
p -> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p Inferred ParamType
forall t. Inferred t
NoneInferred) [PatBase NoInfo VName 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, QualName VName)]
_ (RecordPat [(L Name, PatBase NoInfo VName ParamType)]
p_fs SrcLoc
_) Inferred ParamType
_
  | Just (L Loc
loc Name
f, PatBase NoInfo VName ParamType
_) <- ((L Name, PatBase NoInfo VName ParamType) -> Bool)
-> [(L Name, PatBase NoInfo VName ParamType)]
-> Maybe (L Name, PatBase NoInfo VName ParamType)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
"_" `isPrefixOf`) ([Char] -> Bool)
-> ((L Name, PatBase NoInfo VName ParamType) -> [Char])
-> (L Name, PatBase NoInfo VName ParamType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameToString (Name -> [Char])
-> ((L Name, PatBase NoInfo VName ParamType) -> Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L Name -> Name
forall a. L a -> a
unLoc (L Name -> Name)
-> ((L Name, PatBase NoInfo VName ParamType) -> L Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (L Name, PatBase NoInfo VName ParamType) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, PatBase NoInfo VName ParamType)]
p_fs =
      Loc -> 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 Loc
loc 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 a. Doc a -> Doc a -> Doc a
</> 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, QualName VName)]
sizes p :: PatBase NoInfo VName ParamType
p@(RecordPat [(L Name, PatBase NoInfo VName ParamType)]
p_fs SrcLoc
loc) (Ascribed ParamType
t)
  | Scalar (Record Map Name ParamType
t_fs) <- ParamType
t,
    [(L Name, PatBase NoInfo VName ParamType)]
p_fs' <- ((L Name, PatBase NoInfo VName ParamType)
 -> (L Name, PatBase NoInfo VName ParamType) -> Ordering)
-> [(L Name, PatBase NoInfo VName ParamType)]
-> [(L Name, PatBase NoInfo VName ParamType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((L Name, PatBase NoInfo VName ParamType) -> L Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> (L Name, PatBase NoInfo VName ParamType)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (L Name, PatBase NoInfo VName ParamType) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, PatBase NoInfo VName ParamType)]
p_fs,
    [(Name, ParamType)]
t_fs' <- ((Name, ParamType) -> (Name, ParamType) -> Ordering)
-> [(Name, ParamType)] -> [(Name, ParamType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Name, ParamType) -> Name)
-> (Name, ParamType) -> (Name, ParamType) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Name, ParamType) -> Name
forall a b. (a, b) -> a
fst) (Map Name ParamType -> [(Name, ParamType)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name ParamType
t_fs),
    ((Name, ParamType) -> Name) -> [(Name, ParamType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, ParamType) -> Name
forall a b. (a, b) -> a
fst [(Name, ParamType)]
t_fs' [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== ((L Name, PatBase NoInfo VName ParamType) -> Name)
-> [(L Name, PatBase NoInfo VName ParamType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (L Name -> Name
forall a. L a -> a
unLoc (L Name -> Name)
-> ((L Name, PatBase NoInfo VName ParamType) -> L Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (L Name, PatBase NoInfo VName ParamType) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, PatBase NoInfo VName ParamType)]
p_fs' =
      [(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
-> TermTypeM [(L Name, Pat ParamType)]
-> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((L Name, PatBase NoInfo VName ParamType)
 -> (Name, ParamType) -> TermTypeM (L Name, Pat ParamType))
-> [(L Name, PatBase NoInfo VName ParamType)]
-> [(Name, ParamType)]
-> TermTypeM [(L Name, Pat ParamType)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (L Name, PatBase NoInfo VName ParamType)
-> (Name, ParamType) -> TermTypeM (L Name, Pat ParamType)
forall {a} {a}.
(L a, PatBase NoInfo VName ParamType)
-> (a, ParamType) -> TermTypeM (L a, Pat ParamType)
check [(L Name, PatBase NoInfo VName ParamType)]
p_fs' [(Name, ParamType)]
t_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
  | Bool
otherwise = do
      Map Name StructType
p_fs' <- (PatBase NoInfo VName ParamType -> TermTypeM StructType)
-> Map Name (PatBase NoInfo VName 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 VName ParamType -> TermTypeM StructType
forall a b. a -> b -> a
const (TermTypeM StructType
 -> PatBase NoInfo VName ParamType -> TermTypeM StructType)
-> TermTypeM StructType
-> PatBase NoInfo VName ParamType
-> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Name -> TermTypeM StructType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t") (Map Name (PatBase NoInfo VName ParamType)
 -> TermTypeM (Map Name StructType))
-> Map Name (PatBase NoInfo VName ParamType)
-> TermTypeM (Map Name StructType)
forall a b. (a -> b) -> a -> b
$ [(Name, PatBase NoInfo VName ParamType)]
-> Map Name (PatBase NoInfo VName ParamType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, PatBase NoInfo VName ParamType)]
 -> Map Name (PatBase NoInfo VName ParamType))
-> [(Name, PatBase NoInfo VName ParamType)]
-> Map Name (PatBase NoInfo VName ParamType)
forall a b. (a -> b) -> a -> b
$ ((L Name, PatBase NoInfo VName ParamType)
 -> (Name, PatBase NoInfo VName ParamType))
-> [(L Name, PatBase NoInfo VName ParamType)]
-> [(Name, PatBase NoInfo VName ParamType)]
forall a b. (a -> b) -> [a] -> [b]
map ((L Name -> Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> (Name, PatBase NoInfo VName ParamType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first L Name -> Name
forall a. L a -> a
unLoc) [(L Name, PatBase NoInfo VName ParamType)]
p_fs

      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
p_fs') [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (((L Name, PatBase NoInfo VName ParamType) -> Name)
-> [(L Name, PatBase NoInfo VName ParamType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (L Name -> Name
forall a. L a -> a
unLoc (L Name -> Name)
-> ((L Name, PatBase NoInfo VName ParamType) -> L Name)
-> (L Name, PatBase NoInfo VName ParamType)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (L Name, PatBase NoInfo VName ParamType) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, PatBase NoInfo VName ParamType)]
p_fs)) (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 a. Doc a -> Doc a -> Doc a
<+> PatBase NoInfo VName ParamType -> Doc ()
forall a ann. Pretty a => a -> Doc ann
forall ann. PatBase NoInfo VName ParamType -> Doc ann
pretty PatBase NoInfo VName 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
p_fs')) (ParamType -> StructType
forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
toStruct ParamType
t)
      [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName 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 -> Inferred ParamType)
-> ParamType -> Inferred ParamType
forall a b. (a -> b) -> a -> b
$ Diet -> StructType -> ParamType
forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
toParam Diet
Observe (StructType -> ParamType) -> StructType -> ParamType
forall a b. (a -> b) -> a -> b
$ 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
p_fs')
  where
    check :: (L a, PatBase NoInfo VName ParamType)
-> (a, ParamType) -> TermTypeM (L a, Pat ParamType)
check (L Loc
f_loc a
f, PatBase NoInfo VName ParamType
p_f) (a
_, ParamType
t_f) = (Loc -> a -> L a
forall a. Loc -> a -> L a
L Loc
f_loc a
f,) (Pat ParamType -> (L a, Pat ParamType))
-> TermTypeM (Pat ParamType) -> TermTypeM (L a, Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p_f (ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed ParamType
t_f)
checkPat' [(SizeBinder VName, QualName VName)]
sizes (RecordPat [(L Name, PatBase NoInfo VName ParamType)]
fs SrcLoc
loc) Inferred ParamType
NoneInferred =
  [(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
[(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
-> (Map (L Name) (Pat ParamType) -> [(L Name, Pat ParamType)])
-> Map (L Name) (Pat ParamType)
-> SrcLoc
-> Pat ParamType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (L Name) (Pat ParamType) -> [(L Name, Pat ParamType)]
forall k a. Map k a -> [(k, a)]
M.toList
    (Map (L Name) (Pat ParamType) -> SrcLoc -> Pat ParamType)
-> TermTypeM (Map (L Name) (Pat ParamType))
-> TermTypeM (SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
-> Map (L Name) (PatBase NoInfo VName ParamType)
-> TermTypeM (Map (L 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 (L Name) a -> f (Map (L Name) b)
traverse (\PatBase NoInfo VName ParamType
p -> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p Inferred ParamType
forall t. Inferred t
NoneInferred) ([(L Name, PatBase NoInfo VName ParamType)]
-> Map (L Name) (PatBase NoInfo VName ParamType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(L Name, PatBase NoInfo VName 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, QualName VName)]
sizes (PatAscription PatBase NoInfo VName ParamType
p TypeExp (ExpBase NoInfo VName) VName
t SrcLoc
loc) Inferred ParamType
maybe_outer_t = do
  (TypeExp (ExpBase Info VName) VName
t', ResType
st, [VName]
_) <- TypeExp (ExpBase NoInfo VName) VName
-> TermTypeM (TypeExp (ExpBase Info VName) VName, ResType, [VName])
checkTypeExpNonrigid TypeExp (ExpBase NoInfo VName) VName
t

  case Inferred ParamType
maybe_outer_t of
    Ascribed ParamType
outer_t -> do
      let st_forunify :: StructType
st_forunify = [(SizeBinder VName, QualName VName)] -> StructType -> StructType
nonrigidFor [(SizeBinder VName, QualName VName)]
sizes (StructType -> StructType) -> StructType -> 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 (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatBase f vn t
-> TypeExp (ExpBase f vn) vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat ParamType
 -> TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType)
-> TermTypeM
     (TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p (ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
        TermTypeM
  (TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (TypeExp (ExpBase Info VName) 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 (ExpBase Info VName) VName
-> TermTypeM (TypeExp (ExpBase Info VName) VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp (ExpBase Info VName) 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 (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType
forall (f :: * -> *) vn t.
PatBase f vn t
-> TypeExp (ExpBase f vn) vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat ParamType
 -> TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (Pat ParamType)
-> TermTypeM
     (TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p (ParamType -> Inferred ParamType
forall t. t -> Inferred t
Ascribed (ResType -> ParamType
resToParam ResType
st))
        TermTypeM
  (TypeExp (ExpBase Info VName) VName -> SrcLoc -> Pat ParamType)
-> TermTypeM (TypeExp (ExpBase Info VName) 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 (ExpBase Info VName) VName
-> TermTypeM (TypeExp (ExpBase Info VName) VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp (ExpBase Info VName) 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, QualName 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, QualName 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, QualName VName)]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo VName 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 VName ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo VName 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 a. Doc a -> Doc a -> Doc a
<+> Int -> Doc ()
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([PatBase NoInfo VName ParamType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatBase NoInfo VName ParamType]
ps)
              Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> Doc ()
"constructor arguments, but type provides"
              Doc () -> Doc () -> Doc ()
forall a. Doc a -> Doc a -> Doc a
<+> 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 a. Doc a -> Doc a -> Doc a
<+> Doc ()
"arguments."
      [Pat ParamType]
ps' <- (PatBase NoInfo VName ParamType
 -> Inferred ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo VName ParamType]
-> [Inferred ParamType]
-> TermTypeM [Pat ParamType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes) [PatBase NoInfo VName 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, QualName VName)]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo VName ParamType]
ps SrcLoc
loc) (Ascribed ParamType
t) = do
  StructType
t' <- SrcLoc -> Name -> TermTypeM StructType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [Pat ParamType]
ps' <- [PatBase NoInfo VName ParamType]
-> (PatBase NoInfo VName 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 VName ParamType]
ps ((PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
 -> TermTypeM [Pat ParamType])
-> (PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
-> TermTypeM [Pat ParamType]
forall a b. (a -> b) -> a -> b
$ \PatBase NoInfo VName ParamType
p -> do
    ParamType
p_t <- SrcLoc -> Name -> TermTypeM ParamType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> Name -> m (TypeBase dim als)
newTypeVar (PatBase NoInfo VName ParamType -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf PatBase NoInfo VName ParamType
p) Name
"t"
    [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName 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)
  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, QualName VName)]
sizes (PatConstr Name
n NoInfo ParamType
NoInfo [PatBase NoInfo VName ParamType]
ps SrcLoc
loc) Inferred ParamType
NoneInferred = do
  [Pat ParamType]
ps' <- (PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
-> [PatBase NoInfo VName 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 VName ParamType
p -> [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName ParamType
p Inferred ParamType
forall t. Inferred t
NoneInferred) [PatBase NoInfo VName ParamType]
ps
  ParamType
t <- SrcLoc -> Name -> TermTypeM ParamType
forall als a dim.
(Monoid als, Located a) =>
a -> Name -> TermTypeM (TypeBase dim als)
forall (m :: * -> *) als a dim.
(MonadUnify m, Monoid als, Located a) =>
a -> 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, QualName VName)] ->
  PatBase NoInfo VName (TypeBase Size u) ->
  Inferred StructType ->
  (Pat ParamType -> TermTypeM a) ->
  TermTypeM a
checkPat :: forall u a.
[(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [(SizeBinder VName, QualName VName)]
sizes PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
p Inferred StructType
t Pat ParamType -> TermTypeM a
m = do
  Pat ParamType
p' <-
    Checking -> TermTypeM (Pat ParamType) -> TermTypeM (Pat ParamType)
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (PatBase NoInfo VName StructType -> Inferred StructType -> Checking
CheckingPat ((TypeBase (ExpBase Info VName) u -> StructType)
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> PatBase NoInfo VName StructType
forall a b.
(a -> b) -> PatBase NoInfo VName a -> PatBase NoInfo VName 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 PatBase NoInfo VName (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, QualName VName)]
-> PatBase NoInfo VName ParamType
-> Inferred ParamType
-> TermTypeM (Pat ParamType)
checkPat' [(SizeBinder VName, QualName VName)]
sizes ((TypeBase (ExpBase Info VName) u -> ParamType)
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> PatBase NoInfo VName ParamType
forall a b.
(a -> b) -> PatBase NoInfo VName a -> PatBase NoInfo VName 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) PatBase NoInfo VName (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, QualName VName) -> Bool)
-> [(SizeBinder VName, QualName VName)]
-> [(SizeBinder VName, QualName 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, QualName VName) -> VName)
-> (SizeBinder VName, QualName VName)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName (SizeBinder VName -> VName)
-> ((SizeBinder VName, QualName VName) -> SizeBinder VName)
-> (SizeBinder VName, QualName VName)
-> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SizeBinder VName, QualName VName) -> SizeBinder VName
forall a b. (a, b) -> a
fst) [(SizeBinder VName, QualName VName)]
sizes of
    (SizeBinder VName
size, QualName VName
_) : [(SizeBinder VName, QualName 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 a. Doc a -> Doc a -> Doc a
<+> 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 a. Doc a -> Doc a -> Doc a
<+> Doc ()
"as it is never used as the size of a concrete (non-function) value."
    [] ->
      Pat ParamType -> TermTypeM a
m Pat ParamType
p'

-- | Check and bind a @let@-pattern.
bindingPat ::
  [SizeBinder VName] ->
  PatBase NoInfo VName (TypeBase Size u) ->
  StructType ->
  (Pat ParamType -> TermTypeM a) ->
  TermTypeM a
bindingPat :: forall u a.
[SizeBinder VName]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
p StructType
t Pat ParamType -> TermTypeM a
m = do
  [(SizeBinder VName, QualName VName)]
substs <- (SizeBinder VName -> TermTypeM (SizeBinder VName, QualName VName))
-> [SizeBinder VName]
-> TermTypeM [(SizeBinder VName, QualName 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 VName -> TermTypeM (SizeBinder VName, QualName VName)
mkSizeSubst [SizeBinder VName]
sizes
  [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
forall u a.
[(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [(SizeBinder VName, QualName VName)]
substs PatBase NoInfo VName (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 (PatBase Info VName StructType -> [Ident StructType]
forall (f :: * -> *) vn t. PatBase f vn t -> [IdentBase f vn t]
patIdents ((ParamType -> StructType)
-> Pat ParamType -> PatBase Info VName 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
  where
    mkSizeSubst :: SizeBinder VName -> TermTypeM (SizeBinder VName, QualName VName)
mkSizeSubst SizeBinder VName
v = do
      VName
v' <- 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 -> Name) -> VName -> Name
forall a b. (a -> b) -> a -> b
$ SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName SizeBinder VName
v
      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 -> TermTypeM ()) -> Usage -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
        SizeBinder VName -> Text -> Usage
forall a. Located a => a -> Text -> Usage
mkUsage SizeBinder VName
v Text
"ambiguous size of bound expression"
      (SizeBinder VName, QualName VName)
-> TermTypeM (SizeBinder VName, QualName VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SizeBinder VName
v, VName -> QualName VName
forall v. v -> QualName v
qualName VName
v')

-- | Check and bind type and value parameters.
bindingParams ::
  [TypeParam] ->
  [PatBase NoInfo VName ParamType] ->
  ([Pat ParamType] -> TermTypeM a) ->
  TermTypeM a
bindingParams :: forall a.
[TypeParam]
-> [PatBase NoInfo VName ParamType]
-> ([Pat ParamType] -> TermTypeM a)
-> TermTypeM a
bindingParams [TypeParam]
tps [PatBase NoInfo VName ParamType]
orig_ps [Pat ParamType] -> TermTypeM a
m = [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]
-> [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
-> TermTypeM a
descend [Pat ParamType]
ps' (PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
p : [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
ps) =
        [(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
forall u a.
[(SizeBinder VName, QualName VName)]
-> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
-> Inferred StructType
-> (Pat ParamType -> TermTypeM a)
-> TermTypeM a
checkPat [] PatBase NoInfo VName (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 (PatBase Info VName StructType -> [Ident StructType]
forall (f :: * -> *) vn t. PatBase f vn t -> [IdentBase f vn t]
patIdents (PatBase Info VName StructType -> [Ident StructType])
-> PatBase Info VName StructType -> [Ident StructType]
forall a b. (a -> b) -> a -> b
$ (ParamType -> StructType)
-> Pat ParamType -> PatBase Info VName 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
$ TermTypeM a -> TermTypeM a
forall a. TermTypeM a -> TermTypeM a
incLevel (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat ParamType]
-> [PatBase NoInfo VName (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') [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
ps
      descend [Pat ParamType]
ps' [] = [Pat ParamType] -> TermTypeM a
m ([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'

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