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

import Control.Monad
import Data.Bifunctor
import Data.Either
import Data.List (find, isPrefixOf, 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.Terms.Scope (typeParamIdent)
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 = TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall {t}. VName -> Maybe (Subst t)
onDim
  where
    onDim :: VName -> Maybe (Subst t)
onDim VName
v
      | Just (SizeBinder VName
s, 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 =
          Subst t -> Maybe (Subst t)
forall a. a -> Maybe a
Just (Subst t -> Maybe (Subst t)) -> Subst t -> Maybe (Subst t)
forall a b. (a -> b) -> a -> b
$ Size -> Subst t
forall t. Size -> Subst t
ExpSubst (Size -> Subst t) -> Size -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> SrcLoc -> Size
sizeFromName QualName VName
v' (SizeBinder VName -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder VName
s)
    onDim VName
_ = Maybe (Subst t)
forall a. Maybe a
Nothing

-- | 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 Size -> TermScope Size) -> TermTypeM a -> TermTypeM a
forall a.
(TermScope Size -> TermScope Size) -> TermTypeM a -> TermTypeM a
localScope (TermScope Size -> [Ident StructType] -> TermScope Size
forall {dim}.
TermScope dim
-> [IdentBase Info VName (TypeBase dim NoMode)] -> TermScope dim
`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 dim
-> [IdentBase Info VName (TypeBase dim NoMode)] -> TermScope dim
bindVars = (TermScope dim
 -> IdentBase Info VName (TypeBase dim NoMode) -> TermScope dim)
-> TermScope dim
-> [IdentBase Info VName (TypeBase dim NoMode)]
-> TermScope dim
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TermScope dim
-> IdentBase Info VName (TypeBase dim NoMode) -> TermScope dim
forall {dim}.
TermScope dim
-> IdentBase Info VName (TypeBase dim NoMode) -> TermScope dim
bindVar

    bindVar :: TermScope dim
-> IdentBase Info VName (TypeBase dim NoMode) -> TermScope dim
bindVar TermScope dim
scope (Ident VName
name (Info TypeBase dim NoMode
tp) SrcLoc
_) =
      TermScope dim
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
  lvl <- TermTypeM Int
forall (m :: * -> *). MonadUnify m => m Int
curLevel
  modifyConstraints (<> M.map (lvl,) (M.fromList constraints))
  localScope extend 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 dim -> TermScope dim
extend TermScope dim
scope =
      TermScope dim
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
_) =
      [ (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 o. [VName] -> TypeBase dim o -> RetTypeBase dim o
RetType [] (StructType -> StructRetType) -> StructType -> StructRetType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size NoMode -> StructType
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (NoMode
-> QualName VName -> [TypeArg Size] -> ScalarTypeBase Size NoMode
forall dim o.
o -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim o
TypeVar NoMode
forall a. Monoid a => a
mempty (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) []))
      ]
    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)]

-- | 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} {o}.
SizeBinder vn -> IdentBase Info vn (TypeBase dim o)
sizeWithType [SizeBinder VName]
sizes) TermTypeM a
m
  where
    sizeWithType :: SizeBinder vn -> IdentBase Info vn (TypeBase dim o)
sizeWithType SizeBinder vn
size =
      vn
-> Info (TypeBase dim o)
-> SrcLoc
-> IdentBase Info vn (TypeBase dim o)
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 o -> Info (TypeBase dim o)
forall a. a -> Info a
Info (ScalarTypeBase dim o -> TypeBase dim o
forall dim o. ScalarTypeBase dim o -> TypeBase dim o
Scalar (PrimType -> ScalarTypeBase dim o
forall dim o. PrimType -> ScalarTypeBase dim o
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 :: Ident StructType -> TermTypeM a -> TermTypeM a
bindingIdent :: forall a. Ident StructType -> TermTypeM a -> TermTypeM a
bindingIdent Ident StructType
ident = [Ident StructType] -> TermTypeM a -> TermTypeM a
forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
binding [Ident StructType
ident]

checkPat' ::
  [(SizeBinder VName, QualName VName)] ->
  Pat ParamType ->
  Inferred ParamType ->
  TermTypeM (Pat ParamType)
checkPat' :: [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes (PatParens Pat (TypeBase Size Diet)
p SrcLoc
loc) Inferred (TypeBase Size Diet)
t =
  Pat (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
PatBase f vn t -> SrcLoc -> PatBase f vn t
PatParens (Pat (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
t TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 Pat (TypeBase Size Diet)
p SrcLoc
loc) Inferred (TypeBase Size Diet)
t =
  AttrInfo VName
-> Pat (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
AttrInfo vn -> PatBase f vn t -> SrcLoc -> PatBase f vn t
PatAttr (AttrInfo VName
 -> Pat (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (AttrInfo VName)
-> TermTypeM
     (Pat (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet))
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 (TypeBase Size Diet) -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
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)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
t TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 (Info TypeBase Size Diet
t) SrcLoc
loc) Inferred (TypeBase Size Diet)
NoneInferred = do
  t' <- SrcLoc -> TypeBase Size Diet -> TermTypeM (TypeBase Size Diet)
forall o. SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVars SrcLoc
loc TypeBase Size Diet
t
  pure $ Id name (Info t') loc
checkPat' [(SizeBinder VName, QualName VName)]
_ (Id VName
name (Info TypeBase Size Diet
t1) SrcLoc
loc) (Ascribed TypeBase Size Diet
t2) = do
  t' <- SrcLoc
-> Map VName Liftedness
-> TypeBase () Diet
-> TypeBase Size Diet
-> TermTypeM (TypeBase Size Diet)
forall o.
Substitutable (TypeBase Size o) =>
SrcLoc
-> Map VName Liftedness
-> TypeBase () o
-> TypeBase Size o
-> TermTypeM (TypeBase Size o)
instTyVars SrcLoc
loc Map VName Liftedness
forall a. Monoid a => a
mempty ((Size -> ()) -> TypeBase Size Diet -> TypeBase () Diet
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 (() -> Size -> ()
forall a b. a -> b -> a
const ()) TypeBase Size Diet
t1) TypeBase Size Diet
t2
  pure $ Id name (Info t') loc
checkPat' [(SizeBinder VName, QualName VName)]
_ (Wildcard (Info TypeBase Size Diet
t) SrcLoc
loc) Inferred (TypeBase Size Diet)
NoneInferred = do
  t' <- SrcLoc -> TypeBase Size Diet -> TermTypeM (TypeBase Size Diet)
forall o. SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVars SrcLoc
loc TypeBase Size Diet
t
  pure $ Wildcard (Info t') loc
checkPat' [(SizeBinder VName, QualName VName)]
_ (Wildcard (Info TypeBase Size Diet
t1) SrcLoc
loc) (Ascribed TypeBase Size Diet
t2) = do
  t' <- SrcLoc
-> Map VName Liftedness
-> TypeBase () Diet
-> TypeBase Size Diet
-> TermTypeM (TypeBase Size Diet)
forall o.
Substitutable (TypeBase Size o) =>
SrcLoc
-> Map VName Liftedness
-> TypeBase () o
-> TypeBase Size o
-> TermTypeM (TypeBase Size o)
instTyVars SrcLoc
loc Map VName Liftedness
forall a. Monoid a => a
mempty ((Size -> ()) -> TypeBase Size Diet -> TypeBase () Diet
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 (() -> Size -> ()
forall a b. a -> b -> a
const ()) TypeBase Size Diet
t1) TypeBase Size Diet
t2
  pure $ Wildcard (Info t') loc
checkPat' [(SizeBinder VName, QualName VName)]
sizes (TuplePat [Pat (TypeBase Size Diet)]
ps SrcLoc
loc) (Ascribed TypeBase Size Diet
t)
  | Just [TypeBase Size Diet]
ts <- TypeBase Size Diet -> Maybe [TypeBase Size Diet]
forall dim o. TypeBase dim o -> Maybe [TypeBase dim o]
isTupleRecord TypeBase Size Diet
t,
    [TypeBase Size Diet] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeBase Size Diet]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Pat (TypeBase Size Diet)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pat (TypeBase Size Diet)]
ps =
      [Pat (TypeBase Size Diet)] -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat
        ([Pat (TypeBase Size Diet)] -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM [Pat (TypeBase Size Diet)]
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat (TypeBase Size Diet)
 -> Inferred (TypeBase Size Diet)
 -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Pat (TypeBase Size Diet)]
-> [Inferred (TypeBase Size Diet)]
-> TermTypeM [Pat (TypeBase Size Diet)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes) [Pat (TypeBase Size Diet)]
ps ((TypeBase Size Diet -> Inferred (TypeBase Size Diet))
-> [TypeBase Size Diet] -> [Inferred (TypeBase Size Diet)]
forall a b. (a -> b) -> [a] -> [b]
map TypeBase Size Diet -> Inferred (TypeBase Size Diet)
forall t. t -> Inferred t
Ascribed [TypeBase Size Diet]
ts)
        TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 =
      -- The unsized type checker has already verified that the
      -- pattern matches the type of the bound expression.
      [Char] -> TermTypeM (Pat (TypeBase Size Diet))
forall a. HasCallStack => [Char] -> a
error ([Char] -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Char] -> TermTypeM (Pat (TypeBase Size Diet))
forall a b. (a -> b) -> a -> b
$ [Char]
"checkPat' TuplePat: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> StructType -> [Char]
forall a. Pretty a => a -> [Char]
prettyString (TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct TypeBase Size Diet
t)
checkPat' [(SizeBinder VName, QualName VName)]
sizes (TuplePat [Pat (TypeBase Size Diet)]
ps SrcLoc
loc) Inferred (TypeBase Size Diet)
NoneInferred =
  [Pat (TypeBase Size Diet)] -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
[PatBase f vn t] -> SrcLoc -> PatBase f vn t
TuplePat ([Pat (TypeBase Size Diet)] -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM [Pat (TypeBase Size Diet)]
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat (TypeBase Size Diet) -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Pat (TypeBase Size Diet)]
-> TermTypeM [Pat (TypeBase Size Diet)]
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 (\Pat (TypeBase Size Diet)
p -> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
forall t. Inferred t
NoneInferred) [Pat (TypeBase Size Diet)]
ps TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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, Pat (TypeBase Size Diet))]
p_fs SrcLoc
_) Inferred (TypeBase Size Diet)
_
  | Just (L Loc
loc Name
f, Pat (TypeBase Size Diet)
_) <- ((L Name, Pat (TypeBase Size Diet)) -> Bool)
-> [(L Name, Pat (TypeBase Size Diet))]
-> Maybe (L Name, Pat (TypeBase Size Diet))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
"_" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) ([Char] -> Bool)
-> ((L Name, Pat (TypeBase Size Diet)) -> [Char])
-> (L Name, Pat (TypeBase Size Diet))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameToString (Name -> [Char])
-> ((L Name, Pat (TypeBase Size Diet)) -> Name)
-> (L Name, Pat (TypeBase Size Diet))
-> [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, Pat (TypeBase Size Diet)) -> L Name)
-> (L Name, Pat (TypeBase Size Diet))
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (L Name, Pat (TypeBase Size Diet)) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, Pat (TypeBase Size Diet))]
p_fs =
      Loc -> Notes -> Doc () -> TermTypeM (Pat (TypeBase Size Diet))
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 (TypeBase Size Diet)))
-> Doc () -> TermTypeM (Pat (TypeBase Size Diet))
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 (RecordPat [(L Name, Pat (TypeBase Size Diet))]
p_fs SrcLoc
loc) (Ascribed TypeBase Size Diet
t)
  | Scalar (Record Map Name (TypeBase Size Diet)
t_fs) <- TypeBase Size Diet
t,
    [(L Name, Pat (TypeBase Size Diet))]
p_fs' <- ((L Name, Pat (TypeBase Size Diet))
 -> (L Name, Pat (TypeBase Size Diet)) -> Ordering)
-> [(L Name, Pat (TypeBase Size Diet))]
-> [(L Name, Pat (TypeBase Size Diet))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((L Name, Pat (TypeBase Size Diet)) -> L Name)
-> (L Name, Pat (TypeBase Size Diet))
-> (L Name, Pat (TypeBase Size Diet))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (L Name, Pat (TypeBase Size Diet)) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, Pat (TypeBase Size Diet))]
p_fs,
    [(Name, TypeBase Size Diet)]
t_fs' <- ((Name, TypeBase Size Diet)
 -> (Name, TypeBase Size Diet) -> Ordering)
-> [(Name, TypeBase Size Diet)] -> [(Name, TypeBase Size Diet)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Name, TypeBase Size Diet) -> Name)
-> (Name, TypeBase Size Diet)
-> (Name, TypeBase Size Diet)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Name, TypeBase Size Diet) -> Name
forall a b. (a, b) -> a
fst) (Map Name (TypeBase Size Diet) -> [(Name, TypeBase Size Diet)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name (TypeBase Size Diet)
t_fs),
    ((Name, TypeBase Size Diet) -> Name)
-> [(Name, TypeBase Size Diet)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TypeBase Size Diet) -> Name
forall a b. (a, b) -> a
fst [(Name, TypeBase Size Diet)]
t_fs' [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== ((L Name, Pat (TypeBase Size Diet)) -> Name)
-> [(L Name, Pat (TypeBase Size Diet))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (L Name -> Name
forall a. L a -> a
unLoc (L Name -> Name)
-> ((L Name, Pat (TypeBase Size Diet)) -> L Name)
-> (L Name, Pat (TypeBase Size Diet))
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (L Name, Pat (TypeBase Size Diet)) -> L Name
forall a b. (a, b) -> a
fst) [(L Name, Pat (TypeBase Size Diet))]
p_fs' =
      [(L Name, Pat (TypeBase Size Diet))]
-> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
[(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(L Name, Pat (TypeBase Size Diet))]
 -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM [(L Name, Pat (TypeBase Size Diet))]
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((L Name, Pat (TypeBase Size Diet))
 -> (Name, TypeBase Size Diet)
 -> TermTypeM (L Name, Pat (TypeBase Size Diet)))
-> [(L Name, Pat (TypeBase Size Diet))]
-> [(Name, TypeBase Size Diet)]
-> TermTypeM [(L Name, Pat (TypeBase Size Diet))]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (L Name, Pat (TypeBase Size Diet))
-> (Name, TypeBase Size Diet)
-> TermTypeM (L Name, Pat (TypeBase Size Diet))
forall {a} {a}.
(L a, Pat (TypeBase Size Diet))
-> (a, TypeBase Size Diet)
-> TermTypeM (L a, Pat (TypeBase Size Diet))
check [(L Name, Pat (TypeBase Size Diet))]
p_fs' [(Name, TypeBase Size Diet)]
t_fs' TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 =
      -- The unsized type checker has already verified that the
      -- pattern matches the type of the bound expression.
      [Char] -> TermTypeM (Pat (TypeBase Size Diet))
forall a. HasCallStack => [Char] -> a
error ([Char] -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Char] -> TermTypeM (Pat (TypeBase Size Diet))
forall a b. (a -> b) -> a -> b
$ [Char]
"checkPat' RecordPat: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> StructType -> [Char]
forall a. Pretty a => a -> [Char]
prettyString (TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct TypeBase Size Diet
t)
  where
    check :: (L a, Pat (TypeBase Size Diet))
-> (a, TypeBase Size Diet)
-> TermTypeM (L a, Pat (TypeBase Size Diet))
check (L Loc
f_loc a
f, Pat (TypeBase Size Diet)
p_f) (a
_, TypeBase Size Diet
t_f) = (Loc -> a -> L a
forall a. Loc -> a -> L a
L Loc
f_loc a
f,) (Pat (TypeBase Size Diet) -> (L a, Pat (TypeBase Size Diet)))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM (L a, Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p_f (TypeBase Size Diet -> Inferred (TypeBase Size Diet)
forall t. t -> Inferred t
Ascribed TypeBase Size Diet
t_f)
checkPat' [(SizeBinder VName, QualName VName)]
sizes (RecordPat [(L Name, Pat (TypeBase Size Diet))]
fs SrcLoc
loc) Inferred (TypeBase Size Diet)
NoneInferred =
  [(L Name, Pat (TypeBase Size Diet))]
-> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
[(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
RecordPat ([(L Name, Pat (TypeBase Size Diet))]
 -> SrcLoc -> Pat (TypeBase Size Diet))
-> (Map (L Name) (Pat (TypeBase Size Diet))
    -> [(L Name, Pat (TypeBase Size Diet))])
-> Map (L Name) (Pat (TypeBase Size Diet))
-> SrcLoc
-> Pat (TypeBase Size Diet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (L Name) (Pat (TypeBase Size Diet))
-> [(L Name, Pat (TypeBase Size Diet))]
forall k a. Map k a -> [(k, a)]
M.toList
    (Map (L Name) (Pat (TypeBase Size Diet))
 -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (Map (L Name) (Pat (TypeBase Size Diet)))
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat (TypeBase Size Diet) -> TermTypeM (Pat (TypeBase Size Diet)))
-> Map (L Name) (Pat (TypeBase Size Diet))
-> TermTypeM (Map (L Name) (Pat (TypeBase Size Diet)))
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 (\Pat (TypeBase Size Diet)
p -> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
forall t. Inferred t
NoneInferred) ([(L Name, Pat (TypeBase Size Diet))]
-> Map (L Name) (Pat (TypeBase Size Diet))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(L Name, Pat (TypeBase Size Diet))]
fs)
    TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 Pat (TypeBase Size Diet)
p TypeExp Size VName
t SrcLoc
loc) Inferred (TypeBase Size Diet)
maybe_outer_t = do
  (t', st, _) <- TypeExp Size VName
-> TermTypeM (TypeExp Size VName, ResType, [VName])
checkTypeExpNonrigid TypeExp Size VName
t

  case maybe_outer_t of
    Ascribed TypeBase Size Diet
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 o. TypeBase dim o -> TypeBase dim NoMode
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 (TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct TypeBase Size Diet
outer_t)

      Pat (TypeBase Size Diet)
-> TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
PatBase f vn t
-> TypeExp (ExpBase f vn) vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat (TypeBase Size Diet)
 -> TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM
     (TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p (TypeBase Size Diet -> Inferred (TypeBase Size Diet)
forall t. t -> Inferred t
Ascribed (ResType -> TypeBase Size Diet
resToParam ResType
st))
        TermTypeM
  (TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (TypeExp Size VName)
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp Size VName -> TermTypeM (TypeExp Size VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Size VName
t'
        TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 (TypeBase Size Diet)
NoneInferred ->
      Pat (TypeBase Size Diet)
-> TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet)
forall (f :: * -> *) vn t.
PatBase f vn t
-> TypeExp (ExpBase f vn) vn -> SrcLoc -> PatBase f vn t
PatAscription
        (Pat (TypeBase Size Diet)
 -> TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM
     (TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p (TypeBase Size Diet -> Inferred (TypeBase Size Diet)
forall t. t -> Inferred t
Ascribed (ResType -> TypeBase Size Diet
resToParam ResType
st))
        TermTypeM
  (TypeExp Size VName -> SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM (TypeExp Size VName)
-> TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp Size VName -> TermTypeM (TypeExp Size VName)
forall a. a -> TermTypeM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp Size VName
t'
        TermTypeM (SrcLoc -> Pat (TypeBase Size Diet))
-> TermTypeM SrcLoc -> TermTypeM (Pat (TypeBase Size Diet))
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 (Info TypeBase Size Diet
t) SrcLoc
loc) Inferred (TypeBase Size Diet)
_ = do
  t' <- SrcLoc -> TypeBase Size Diet -> TermTypeM (TypeBase Size Diet)
forall o. SrcLoc -> TypeBase Size o -> TermTypeM (TypeBase Size o)
replaceTyVars SrcLoc
loc TypeBase Size Diet
t
  pure $ PatLit l (Info t') loc
checkPat' [(SizeBinder VName, QualName VName)]
sizes (PatConstr Name
n Info (TypeBase Size Diet)
info [Pat (TypeBase Size Diet)]
ps SrcLoc
loc) Inferred (TypeBase Size Diet)
NoneInferred = do
  ps' <- (Pat (TypeBase Size Diet) -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Pat (TypeBase Size Diet)]
-> TermTypeM [Pat (TypeBase Size Diet)]
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 (\Pat (TypeBase Size Diet)
p -> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
forall t. Inferred t
NoneInferred) [Pat (TypeBase Size Diet)]
ps
  pure $ PatConstr n info ps' loc
checkPat' [(SizeBinder VName, QualName VName)]
sizes (PatConstr Name
n Info (TypeBase Size Diet)
_ [Pat (TypeBase Size Diet)]
ps SrcLoc
loc) (Ascribed (Scalar (Sum Map Name [TypeBase Size Diet]
cs)))
  | Just [TypeBase Size Diet]
ts <- Name -> Map Name [TypeBase Size Diet] -> Maybe [TypeBase Size Diet]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name [TypeBase Size Diet]
cs = do
      ps' <- (Pat (TypeBase Size Diet)
 -> TypeBase Size Diet -> TermTypeM (Pat (TypeBase Size Diet)))
-> [Pat (TypeBase Size Diet)]
-> [TypeBase Size Diet]
-> TermTypeM [Pat (TypeBase Size Diet)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Pat (TypeBase Size Diet)
p TypeBase Size Diet
t -> [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p (TypeBase Size Diet -> Inferred (TypeBase Size Diet)
forall t. t -> Inferred t
Ascribed TypeBase Size Diet
t)) [Pat (TypeBase Size Diet)]
ps [TypeBase Size Diet]
ts
      pure $ PatConstr n (Info (Scalar (Sum cs))) ps' loc
checkPat' [(SizeBinder VName, QualName VName)]
_ Pat (TypeBase Size Diet)
p Inferred (TypeBase Size Diet)
t =
  [Char] -> TermTypeM (Pat (TypeBase Size Diet))
forall a. HasCallStack => [Char] -> a
error ([Char] -> TermTypeM (Pat (TypeBase Size Diet)))
-> ([[Char]] -> [Char])
-> [[Char]]
-> TermTypeM (Pat (TypeBase Size Diet))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
unlines ([[Char]] -> TermTypeM (Pat (TypeBase Size Diet)))
-> [[Char]] -> TermTypeM (Pat (TypeBase Size Diet))
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"checkPat': bad case",
      Pat (TypeBase Size Diet) -> [Char]
forall a. Pretty a => a -> [Char]
prettyString Pat (TypeBase Size Diet)
p,
      Inferred (TypeBase Size Diet) -> [Char]
forall a. Show a => a -> [Char]
show Inferred (TypeBase Size Diet)
t
    ]

checkPat ::
  [(SizeBinder VName, QualName VName)] ->
  Pat ParamType ->
  Inferred StructType ->
  (Pat ParamType -> TermTypeM a) ->
  TermTypeM a
checkPat :: forall a.
[(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
checkPat [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p Inferred StructType
t Pat (TypeBase Size Diet) -> TermTypeM a
m = do
  p' <-
    Checking
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (PatBase Info VName StructType -> Inferred StructType -> Checking
CheckingPat ((TypeBase Size Diet -> StructType)
-> Pat (TypeBase Size Diet) -> 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 TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct Pat (TypeBase Size Diet)
p) Inferred StructType
t) (TermTypeM (Pat (TypeBase Size Diet))
 -> TermTypeM (Pat (TypeBase Size Diet)))
-> TermTypeM (Pat (TypeBase Size Diet))
-> TermTypeM (Pat (TypeBase Size Diet))
forall a b. (a -> b) -> a -> b
$
      [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred (TypeBase Size Diet)
-> TermTypeM (Pat (TypeBase Size Diet))
checkPat' [(SizeBinder VName, QualName VName)]
sizes Pat (TypeBase Size Diet)
p ((StructType -> TypeBase Size Diet)
-> Inferred StructType -> Inferred (TypeBase Size Diet)
forall a b. (a -> b) -> Inferred a -> Inferred b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Diet -> StructType -> TypeBase Size Diet
forall o. Diet -> TypeBase Size o -> TypeBase Size Diet
toParam Diet
Observe) Inferred StructType
t)

  let explicit = StructType -> Set VName
mustBeExplicitInType (StructType -> Set VName) -> StructType -> Set VName
forall a b. (a -> b) -> a -> b
$ Pat (TypeBase Size Diet) -> StructType
forall o. Pat (TypeBase Size o) -> StructType
patternStructType Pat (TypeBase Size Diet)
p'

  case filter ((`S.member` explicit) . sizeName . fst) 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 (TypeBase Size Diet) -> TermTypeM a
m Pat (TypeBase Size Diet)
p'

-- | Check and bind a single parameter.
bindingParam ::
  Pat ParamType ->
  StructType ->
  (Pat ParamType -> TermTypeM a) ->
  TermTypeM a
bindingParam :: forall a.
Pat (TypeBase Size Diet)
-> StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
bindingParam Pat (TypeBase Size Diet)
p StructType
t Pat (TypeBase Size Diet) -> TermTypeM a
m = do
  [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
forall a.
[(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
checkPat [(SizeBinder VName, QualName VName)]
forall a. Monoid a => a
mempty Pat (TypeBase Size Diet)
p (StructType -> Inferred StructType
forall t. t -> Inferred t
Ascribed StructType
t) ((Pat (TypeBase Size Diet) -> TermTypeM a) -> TermTypeM a)
-> (Pat (TypeBase Size Diet) -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat (TypeBase Size Diet)
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 ((TypeBase Size Diet -> StructType)
-> Pat (TypeBase Size Diet) -> 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 TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct Pat (TypeBase Size Diet)
p')) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ Pat (TypeBase Size Diet) -> TermTypeM a
m Pat (TypeBase Size Diet)
p'

-- | Check and bind a @let@-pattern.
bindingPat ::
  [SizeBinder VName] ->
  Pat (TypeBase Size o) ->
  StructType ->
  (Pat ParamType -> TermTypeM a) ->
  TermTypeM a
bindingPat :: forall o a.
[SizeBinder VName]
-> Pat (TypeBase Size o)
-> StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes Pat (TypeBase Size o)
p StructType
t Pat (TypeBase Size Diet) -> TermTypeM a
m = do
  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
  checkPat substs (fmap (toParam Observe) p) (Ascribed t) $ \Pat (TypeBase Size Diet)
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 ((TypeBase Size Diet -> StructType)
-> Pat (TypeBase Size Diet) -> 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 TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct Pat (TypeBase Size Diet)
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 (TypeBase Size Diet) -> FV
forall o. Pat (TypeBase Size o) -> FV
freeInPat Pat (TypeBase Size Diet)
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 (TypeBase Size Diet) -> TermTypeM a
m Pat (TypeBase Size Diet)
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
      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
      constrain v' . Size Nothing $
        mkUsage v "ambiguous size of bound expression"
      pure (v, qualName v')

-- | Check and bind type and value parameters.
bindingParams ::
  [TypeParam] ->
  [Pat ParamType] ->
  ([Pat ParamType] -> TermTypeM a) ->
  TermTypeM a
bindingParams :: forall a.
[TypeParam]
-> [Pat (TypeBase Size Diet)]
-> ([Pat (TypeBase Size Diet)] -> TermTypeM a)
-> TermTypeM a
bindingParams [TypeParam]
tps [Pat (TypeBase Size Diet)]
orig_ps [Pat (TypeBase Size Diet)] -> 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 (TypeBase Size Diet)]
-> [Pat (TypeBase Size Diet)] -> TermTypeM a
descend [Pat (TypeBase Size Diet)]
ps' (Pat (TypeBase Size Diet)
p : [Pat (TypeBase Size Diet)]
ps) =
        [(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
forall a.
[(SizeBinder VName, QualName VName)]
-> Pat (TypeBase Size Diet)
-> Inferred StructType
-> (Pat (TypeBase Size Diet) -> TermTypeM a)
-> TermTypeM a
checkPat [] Pat (TypeBase Size Diet)
p Inferred StructType
forall t. Inferred t
NoneInferred ((Pat (TypeBase Size Diet) -> TermTypeM a) -> TermTypeM a)
-> (Pat (TypeBase Size Diet) -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat (TypeBase Size Diet)
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
$ (TypeBase Size Diet -> StructType)
-> Pat (TypeBase Size Diet) -> 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 TypeBase Size Diet -> StructType
forall dim o. TypeBase dim o -> TypeBase dim NoMode
toStruct Pat (TypeBase Size Diet)
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 (TypeBase Size Diet)]
-> [Pat (TypeBase Size Diet)] -> TermTypeM a
descend (Pat (TypeBase Size Diet)
p' Pat (TypeBase Size Diet)
-> [Pat (TypeBase Size Diet)] -> [Pat (TypeBase Size Diet)]
forall a. a -> [a] -> [a]
: [Pat (TypeBase Size Diet)]
ps') [Pat (TypeBase Size Diet)]
ps
      descend [Pat (TypeBase Size Diet)]
ps' [] = [Pat (TypeBase Size Diet)] -> TermTypeM a
m ([Pat (TypeBase Size Diet)] -> TermTypeM a)
-> [Pat (TypeBase Size Diet)] -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat (TypeBase Size Diet)] -> [Pat (TypeBase Size Diet)]
forall a. [a] -> [a]
reverse [Pat (TypeBase Size Diet)]
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 (TypeBase Size Diet)]
-> [Pat (TypeBase Size Diet)] -> TermTypeM a
descend [] [Pat (TypeBase Size Diet)]
orig_ps