{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}

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

import Control.Monad.Except
import Control.Monad.State
import Data.Bitraversable
import Data.Either
import Data.List (find, isPrefixOf, sort)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Util.Pretty hiding (bool, group, space)
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Terms.Monad
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify hiding (Usage)
import Prelude hiding (mod)

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

nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor :: [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor [] StructType
t = StructType -> TermTypeM StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t -- Minor optimisation.
nonrigidFor [SizeBinder VName]
sizes StructType
t = StateT [(VName, VName)] TermTypeM StructType
-> [(VName, VName)] -> TermTypeM StructType
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((DimDecl VName
 -> StateT [(VName, VName)] TermTypeM (DimDecl VName))
-> (() -> StateT [(VName, VName)] TermTypeM ())
-> StructType
-> StateT [(VName, VName)] TermTypeM StructType
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse DimDecl VName -> StateT [(VName, VName)] TermTypeM (DimDecl VName)
forall (t :: (* -> *) -> * -> *).
(MonadState [(VName, VName)] (t TermTypeM), MonadTrans t) =>
DimDecl VName -> t TermTypeM (DimDecl VName)
onDim () -> StateT [(VName, VName)] TermTypeM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t) [(VName, VName)]
forall a. Monoid a => a
mempty
  where
    onDim :: DimDecl VName -> t TermTypeM (DimDecl VName)
onDim (NamedDim (QualName [VName]
_ VName
v))
      | Just SizeBinder VName
size <- (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> Maybe (SizeBinder VName)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
v) (VName -> Bool)
-> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes = do
          Maybe VName
prev <- ([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName))
-> ([(VName, VName)] -> Maybe VName) -> t TermTypeM (Maybe VName)
forall a b. (a -> b) -> a -> b
$ VName -> [(VName, VName)] -> Maybe VName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VName
v
          case Maybe VName
prev of
            Maybe VName
Nothing -> do
              VName
v' <- TermTypeM VName -> t TermTypeM VName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM VName -> t TermTypeM VName)
-> TermTypeM VName -> t TermTypeM VName
forall a b. (a -> b) -> a -> b
$ Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID (Name -> TermTypeM VName) -> Name -> TermTypeM VName
forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
v
              TermTypeM () -> t TermTypeM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TermTypeM () -> t TermTypeM ()) -> TermTypeM () -> t TermTypeM ()
forall a b. (a -> b) -> a -> b
$ VName -> Constraint -> TermTypeM ()
constrain VName
v' (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ Maybe (DimDecl VName) -> Usage -> Constraint
Size Maybe (DimDecl VName)
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Usage
mkUsage' (SrcLoc -> Usage) -> SrcLoc -> Usage
forall a b. (a -> b) -> a -> b
$ SizeBinder VName -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder VName
size
              ([(VName, VName)] -> [(VName, VName)]) -> t TermTypeM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((VName
v, VName
v') (VName, VName) -> [(VName, VName)] -> [(VName, VName)]
forall a. a -> [a] -> [a]
:)
              DimDecl VName -> t TermTypeM (DimDecl VName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DimDecl VName -> t TermTypeM (DimDecl VName))
-> DimDecl VName -> t TermTypeM (DimDecl VName)
forall a b. (a -> b) -> a -> b
$ QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
v'
            Just VName
v' ->
              DimDecl VName -> t TermTypeM (DimDecl VName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DimDecl VName -> t TermTypeM (DimDecl VName))
-> DimDecl VName -> t TermTypeM (DimDecl VName)
forall a b. (a -> b) -> a -> b
$ QualName VName -> DimDecl VName
forall vn. QualName vn -> DimDecl vn
NamedDim (QualName VName -> DimDecl VName)
-> QualName VName -> DimDecl VName
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
v'
    onDim DimDecl VName
d = DimDecl VName -> t TermTypeM (DimDecl VName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure DimDecl VName
d

-- | The set of in-scope variables that are being aliased.
boundAliases :: Aliasing -> S.Set VName
boundAliases :: Aliasing -> Set VName
boundAliases = (Alias -> VName) -> Aliasing -> Set VName
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar (Aliasing -> Set VName)
-> (Aliasing -> Aliasing) -> Aliasing -> Set VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Alias -> Bool) -> Aliasing -> Aliasing
forall a. (a -> Bool) -> Set a -> Set a
S.filter Alias -> Bool
bound
  where
    bound :: Alias -> Bool
bound AliasBound {} = Bool
True
    bound AliasFree {} = Bool
False

checkIfUsed :: Bool -> Occurrences -> Ident -> TermTypeM ()
checkIfUsed :: Bool -> Occurrences -> Ident -> TermTypeM ()
checkIfUsed Bool
allow_consume Occurrences
occs Ident
v
  | Bool -> Bool
not Bool
allow_consume,
    Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> Bool
forall shape as. TypeBase shape as -> Bool
unique (TypeBase (DimDecl VName) Aliasing -> Bool)
-> TypeBase (DimDecl VName) Aliasing -> Bool
forall a b. (a -> b) -> a -> b
$ Info (TypeBase (DimDecl VName) Aliasing)
-> TypeBase (DimDecl VName) Aliasing
forall a. Info a -> a
unInfo (Info (TypeBase (DimDecl VName) Aliasing)
 -> TypeBase (DimDecl VName) Aliasing)
-> Info (TypeBase (DimDecl VName) Aliasing)
-> TypeBase (DimDecl VName) Aliasing
forall a b. (a -> b) -> a -> b
$ Ident -> Info (TypeBase (DimDecl VName) Aliasing)
forall (f :: * -> *) vn.
IdentBase f vn -> f (TypeBase (DimDecl VName) Aliasing)
identType Ident
v,
    Just Occurrence
occ <- (Occurrence -> Bool) -> Occurrences -> Maybe Occurrence
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Occurrence -> Bool
consumes Occurrences
occs =
      SrcLoc -> Notes -> Doc -> TermTypeM ()
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError (Occurrence -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Occurrence
occ) Notes
forall a. Monoid a => a
mempty (Doc -> TermTypeM ()) -> Doc -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
        Doc
"Consuming"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName (VName -> Doc) -> VName -> Doc
forall a b. (a -> b) -> a -> b
$ Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v)
          Doc -> Doc -> Doc
<+> String -> Doc
textwrap (String
"which is a non-consumable parameter bound at " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Loc -> String
forall a. Located a => a -> String
locStr (Ident -> Loc
forall a. Located a => a -> Loc
locOf Ident
v) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".")
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Occurrences -> Set VName
allOccurring Occurrences
occs,
    Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String
"_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` VName -> String
forall v. IsName v => v -> String
prettyName (Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v) =
      SrcLoc -> Doc -> TermTypeM ()
forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc -> m ()
warn (Ident -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Ident
v) (Doc -> TermTypeM ()) -> Doc -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
        Doc
"Unused variable" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName (VName -> Doc) -> VName -> Doc
forall a b. (a -> b) -> a -> b
$ Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v) Doc -> Doc -> Doc
<+> Doc
"."
  | Bool
otherwise =
      () -> TermTypeM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    consumes :: Occurrence -> Bool
consumes = Bool -> (Set VName -> Bool) -> Maybe (Set VName) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member`) (Maybe (Set VName) -> Bool)
-> (Occurrence -> Maybe (Set VName)) -> Occurrence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Occurrence -> Maybe (Set VName)
consumed

-- | Bind these identifiers locally while running the provided action.
-- Checks that the identifiers are used properly within the scope
-- (e.g. consumption).
binding ::
  -- | Allow consumption, even if the type is not unique.
  Bool ->
  [Ident] ->
  TermTypeM a ->
  TermTypeM a
binding :: Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
allow_consume [Ident]
idents = TermTypeM a -> TermTypeM a
forall b. TermTypeM b -> TermTypeM b
check (TermTypeM a -> TermTypeM a)
-> (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermTypeM a -> TermTypeM a
forall b. TermTypeM b -> TermTypeM b
handleVars
  where
    handleVars :: TermTypeM a -> TermTypeM a
handleVars TermTypeM a
m =
      (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope (TermScope -> [Ident] -> TermScope
`bindVars` [Ident]
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] -> (Ident -> TermTypeM ()) -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident]
idents ((Ident -> TermTypeM ()) -> TermTypeM ())
-> (Ident -> TermTypeM ()) -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ \Ident
ident ->
          VName -> Constraint -> TermTypeM ()
constrain (Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
ident) (Constraint -> TermTypeM ()) -> Constraint -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Constraint
ParamSize (SrcLoc -> Constraint) -> SrcLoc -> Constraint
forall a b. (a -> b) -> a -> b
$ Ident -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Ident
ident
        TermTypeM a
m

    bindVars :: TermScope -> [Ident] -> TermScope
    bindVars :: TermScope -> [Ident] -> TermScope
bindVars = (TermScope -> Ident -> TermScope)
-> TermScope -> [Ident] -> TermScope
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TermScope -> Ident -> TermScope
bindVar

    bindVar :: TermScope -> Ident -> TermScope
    bindVar :: TermScope -> Ident -> TermScope
bindVar TermScope
scope (Ident VName
name (Info TypeBase (DimDecl VName) Aliasing
tp) SrcLoc
_) =
      let inedges :: Set VName
inedges = Aliasing -> Set VName
boundAliases (Aliasing -> Set VName) -> Aliasing -> Set VName
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> Aliasing
forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase (DimDecl VName) Aliasing
tp
          update :: ValBinding -> ValBinding
update (BoundV Locality
l [TypeParam]
tparams TypeBase (DimDecl VName) Aliasing
in_t)
            | Array {} <- TypeBase (DimDecl VName) Aliasing
tp = Locality
-> [TypeParam] -> TypeBase (DimDecl VName) Aliasing -> ValBinding
BoundV Locality
l [TypeParam]
tparams (TypeBase (DimDecl VName) Aliasing
in_t TypeBase (DimDecl VName) Aliasing
-> (Aliasing -> Aliasing) -> TypeBase (DimDecl VName) Aliasing
forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` Alias -> Aliasing -> Aliasing
forall a. Ord a => a -> Set a -> Set a
S.insert (VName -> Alias
AliasBound VName
name))
            | Bool
otherwise = Locality
-> [TypeParam] -> TypeBase (DimDecl VName) Aliasing -> ValBinding
BoundV Locality
l [TypeParam]
tparams TypeBase (DimDecl VName) Aliasing
in_t
          update ValBinding
b = ValBinding
b

          tp' :: TypeBase (DimDecl VName) Aliasing
tp' = TypeBase (DimDecl VName) Aliasing
tp TypeBase (DimDecl VName) Aliasing
-> (Aliasing -> Aliasing) -> TypeBase (DimDecl VName) Aliasing
forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` Alias -> Aliasing -> Aliasing
forall a. Ord a => a -> Set a -> Set a
S.insert (VName -> Alias
AliasBound VName
name)
       in TermScope
scope
            { scopeVtable :: Map VName ValBinding
scopeVtable =
                VName -> ValBinding -> Map VName ValBinding -> Map VName ValBinding
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name (Locality
-> [TypeParam] -> TypeBase (DimDecl VName) Aliasing -> ValBinding
BoundV Locality
Local [] TypeBase (DimDecl VName) Aliasing
tp') (Map VName ValBinding -> Map VName ValBinding)
-> Map VName ValBinding -> Map VName ValBinding
forall a b. (a -> b) -> a -> b
$
                  (ValBinding -> ValBinding)
-> Set VName -> Map VName ValBinding -> Map VName ValBinding
forall (t :: * -> *) k a.
(Foldable t, Ord k) =>
(a -> a) -> t k -> Map k a -> Map k a
adjustSeveral ValBinding -> ValBinding
update Set VName
inedges (Map VName ValBinding -> Map VName ValBinding)
-> Map VName ValBinding -> Map VName ValBinding
forall a b. (a -> b) -> a -> b
$
                    TermScope -> Map VName ValBinding
scopeVtable TermScope
scope
            }

    adjustSeveral :: (a -> a) -> t k -> Map k a -> Map k a
adjustSeveral a -> a
f = (Map k a -> t k -> Map k a) -> t k -> Map k a -> Map k a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Map k a -> t k -> Map k a) -> t k -> Map k a -> Map k a)
-> (Map k a -> t k -> Map k a) -> t k -> Map k a -> Map k a
forall a b. (a -> b) -> a -> b
$ (Map k a -> k -> Map k a) -> Map k a -> t k -> Map k a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Map k a -> k -> Map k a) -> Map k a -> t k -> Map k a)
-> (Map k a -> k -> Map k a) -> Map k a -> t k -> Map k a
forall a b. (a -> b) -> a -> b
$ (k -> Map k a -> Map k a) -> Map k a -> k -> Map k a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((k -> Map k a -> Map k a) -> Map k a -> k -> Map k a)
-> (k -> Map k a -> Map k a) -> Map k a -> k -> Map k a
forall a b. (a -> b) -> a -> b
$ (a -> a) -> k -> Map k a -> Map k a
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust a -> a
f

    -- Check whether the bound variables have been used correctly
    -- within their scope.
    check :: TermTypeM b -> TermTypeM b
check TermTypeM b
m = do
      (b
a, Occurrences
usages) <- TermTypeM b -> TermTypeM (b, Occurrences)
forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectBindingsOccurrences TermTypeM b
m
      Occurrences -> TermTypeM ()
checkOccurrences Occurrences
usages

      (Ident -> TermTypeM ()) -> [Ident] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> Occurrences -> Ident -> TermTypeM ()
checkIfUsed Bool
allow_consume Occurrences
usages) [Ident]
idents

      b -> TermTypeM b
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
a

    -- Collect and remove all occurences of @idents@.  This relies
    -- on the fact that no variables shadow any other.
    collectBindingsOccurrences :: TermTypeM a -> TermTypeM (a, Occurrences)
collectBindingsOccurrences TermTypeM a
m = do
      (a
x, Occurrences
usage) <- TermTypeM a -> TermTypeM (a, Occurrences)
forall a. TermTypeM a -> TermTypeM (a, Occurrences)
collectOccurrences TermTypeM a
m
      let (Occurrences
relevant, Occurrences
rest) = Occurrences -> (Occurrences, Occurrences)
split Occurrences
usage
      Occurrences -> TermTypeM ()
occur Occurrences
rest
      (a, Occurrences) -> TermTypeM (a, Occurrences)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, Occurrences
relevant)
      where
        onOcc :: Occurrence -> (Occurrence, Occurrence)
onOcc Occurrence
occ =
          let (Set VName
obs1, Set VName
obs2) = Set VName -> (Set VName, Set VName)
divide (Set VName -> (Set VName, Set VName))
-> Set VName -> (Set VName, Set VName)
forall a b. (a -> b) -> a -> b
$ Occurrence -> Set VName
observed Occurrence
occ
              occ_cons :: Maybe (Set VName, Set VName)
occ_cons = Set VName -> (Set VName, Set VName)
divide (Set VName -> (Set VName, Set VName))
-> Maybe (Set VName) -> Maybe (Set VName, Set VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Occurrence -> Maybe (Set VName)
consumed Occurrence
occ
              con1 :: Maybe (Set VName)
con1 = (Set VName, Set VName) -> Set VName
forall a b. (a, b) -> a
fst ((Set VName, Set VName) -> Set VName)
-> Maybe (Set VName, Set VName) -> Maybe (Set VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Set VName, Set VName)
occ_cons
              con2 :: Maybe (Set VName)
con2 = (Set VName, Set VName) -> Set VName
forall a b. (a, b) -> b
snd ((Set VName, Set VName) -> Set VName)
-> Maybe (Set VName, Set VName) -> Maybe (Set VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Set VName, Set VName)
occ_cons
           in ( Occurrence
occ {observed :: Set VName
observed = Set VName
obs1, consumed :: Maybe (Set VName)
consumed = Maybe (Set VName)
con1},
                Occurrence
occ {observed :: Set VName
observed = Set VName
obs2, consumed :: Maybe (Set VName)
consumed = Maybe (Set VName)
con2}
              )
        split :: Occurrences -> (Occurrences, Occurrences)
split = [(Occurrence, Occurrence)] -> (Occurrences, Occurrences)
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Occurrence, Occurrence)] -> (Occurrences, Occurrences))
-> (Occurrences -> [(Occurrence, Occurrence)])
-> Occurrences
-> (Occurrences, Occurrences)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Occurrence -> (Occurrence, Occurrence))
-> Occurrences -> [(Occurrence, Occurrence)]
forall a b. (a -> b) -> [a] -> [b]
map Occurrence -> (Occurrence, Occurrence)
onOcc
        names :: Set VName
names = [VName] -> Set VName
forall a. Ord a => [a] -> Set a
S.fromList ([VName] -> Set VName) -> [VName] -> Set VName
forall a b. (a -> b) -> a -> b
$ (Ident -> VName) -> [Ident] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> VName
forall (f :: * -> *) vn. IdentBase f vn -> vn
identName [Ident]
idents
        divide :: Set VName -> (Set VName, Set VName)
divide Set VName
s = (Set VName
s Set VName -> Set VName -> Set VName
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set VName
names, Set VName
s Set VName -> Set VName -> Set VName
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set VName
names)

bindingTypes ::
  [Either (VName, TypeBinding) (VName, Constraint)] ->
  TermTypeM a ->
  TermTypeM a
bindingTypes :: [Either (VName, TypeBinding) (VName, Constraint)]
-> TermTypeM a -> TermTypeM a
bindingTypes [Either (VName, TypeBinding) (VName, Constraint)]
types TermTypeM a
m = do
  Level
lvl <- TermTypeM Level
forall (m :: * -> *). MonadUnify m => m Level
curLevel
  (Constraints -> Constraints) -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints (Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<> (Constraint -> (Level, Constraint))
-> Map VName Constraint -> Constraints
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Level
lvl,) ([(VName, Constraint)] -> Map VName Constraint
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, Constraint)]
constraints))
  (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
forall a. (TermScope -> TermScope) -> TermTypeM a -> TermTypeM a
localScope TermScope -> TermScope
extend TermTypeM a
m
  where
    ([(VName, TypeBinding)]
tbinds, [(VName, Constraint)]
constraints) = [Either (VName, TypeBinding) (VName, Constraint)]
-> ([(VName, TypeBinding)], [(VName, Constraint)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (VName, TypeBinding) (VName, Constraint)]
types
    extend :: TermScope -> TermScope
extend TermScope
scope =
      TermScope
scope
        { scopeTypeTable :: Map VName TypeBinding
scopeTypeTable = [(VName, TypeBinding)] -> Map VName TypeBinding
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, TypeBinding)]
tbinds Map VName TypeBinding
-> Map VName TypeBinding -> Map VName TypeBinding
forall a. Semigroup a => a -> a -> a
<> TermScope -> Map VName TypeBinding
scopeTypeTable TermScope
scope
        }

bindingTypeParams :: [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams :: [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams [TypeParam]
tparams =
  Bool -> [Ident] -> TermTypeM a -> TermTypeM a
forall a. Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
False ((TypeParam -> Maybe Ident) -> [TypeParam] -> [Ident]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe Ident
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 (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (()
-> Uniqueness
-> TypeName
-> [TypeArg (DimDecl VName)]
-> ScalarTypeBase (DimDecl VName) ()
forall dim as.
as
-> Uniqueness -> TypeName -> [TypeArg dim] -> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (VName -> TypeName
typeName VName
v) [])),
        (VName, Constraint)
-> Either (VName, TypeBinding) (VName, Constraint)
forall a b. b -> Either a b
Right (VName
v, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l SrcLoc
loc)
      ]
    typeParamType (TypeParamDim VName
v SrcLoc
loc) =
      [(VName, Constraint)
-> Either (VName, TypeBinding) (VName, Constraint)
forall a b. b -> Either a b
Right (VName
v, SrcLoc -> Constraint
ParamSize SrcLoc
loc)]

typeParamIdent :: TypeParam -> Maybe Ident
typeParamIdent :: TypeParam -> Maybe Ident
typeParamIdent (TypeParamDim VName
v SrcLoc
loc) =
  Ident -> Maybe Ident
forall a. a -> Maybe a
Just (Ident -> Maybe Ident) -> Ident -> Maybe Ident
forall a b. (a -> b) -> a -> b
$ VName
-> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Ident
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase f vn
Ident VName
v (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (TypeBase (DimDecl VName) Aliasing
 -> Info (TypeBase (DimDecl VName) Aliasing))
-> TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) Aliasing
 -> TypeBase (DimDecl VName) Aliasing)
-> ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (DimDecl VName) Aliasing
forall dim as. PrimType -> ScalarTypeBase dim as
Prim (PrimType -> ScalarTypeBase (DimDecl VName) Aliasing)
-> PrimType -> ScalarTypeBase (DimDecl VName) Aliasing
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) SrcLoc
loc
typeParamIdent TypeParam
_ = Maybe Ident
forall a. Maybe a
Nothing

-- | Bind a single term-level identifier.
bindingIdent ::
  IdentBase NoInfo Name ->
  PatType ->
  (Ident -> TermTypeM a) ->
  TermTypeM a
bindingIdent :: IdentBase NoInfo Name
-> TypeBase (DimDecl VName) Aliasing
-> (Ident -> TermTypeM a)
-> TermTypeM a
bindingIdent (Ident Name
v NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
vloc) TypeBase (DimDecl VName) Aliasing
t Ident -> TermTypeM a
m =
  [(Namespace, Name)] -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
v)] (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    VName
v' <- Namespace -> Name -> SrcLoc -> TermTypeM VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
vloc
    let ident :: Ident
ident = VName
-> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Ident
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase f vn
Ident VName
v' (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info TypeBase (DimDecl VName) Aliasing
t) SrcLoc
vloc
    Bool -> [Ident] -> TermTypeM a -> TermTypeM a
forall a. Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
True [Ident
ident] (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ Ident -> TermTypeM a
m Ident
ident

-- | Bind @let@-bound sizes.  This is usually followed by 'bindingPat'
-- immediately afterwards.
bindingSizes :: [SizeBinder Name] -> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes :: [SizeBinder Name]
-> ([SizeBinder VName] -> TermTypeM a) -> TermTypeM a
bindingSizes [] [SizeBinder VName] -> TermTypeM a
m = [SizeBinder VName] -> TermTypeM a
m [] -- Minor optimisation.
bindingSizes [SizeBinder Name]
sizes [SizeBinder VName] -> TermTypeM a
m = do
  (Map Name SrcLoc -> SizeBinder Name -> TermTypeM (Map Name SrcLoc))
-> Map Name SrcLoc -> [SizeBinder Name] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ Map Name SrcLoc -> SizeBinder Name -> TermTypeM (Map Name SrcLoc)
forall k (m :: * -> *).
(Ord k, MonadTypeChecker m) =>
Map k SrcLoc -> SizeBinder k -> m (Map k SrcLoc)
lookForDuplicates Map Name SrcLoc
forall a. Monoid a => a
mempty [SizeBinder Name]
sizes
  [(Namespace, Name)] -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced ((SizeBinder Name -> (Namespace, Name))
-> [SizeBinder Name] -> [(Namespace, Name)]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder Name -> (Namespace, Name)
forall b. SizeBinder b -> (Namespace, b)
sizeWithSpace [SizeBinder Name]
sizes) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    [SizeBinder VName]
sizes' <- (SizeBinder Name -> TermTypeM (SizeBinder VName))
-> [SizeBinder Name] -> TermTypeM [SizeBinder VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SizeBinder Name -> TermTypeM (SizeBinder VName)
forall (f :: * -> *).
MonadTypeChecker f =>
SizeBinder Name -> f (SizeBinder VName)
check [SizeBinder Name]
sizes
    Bool -> [Ident] -> TermTypeM a -> TermTypeM a
forall a. Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
False ((SizeBinder VName -> Ident) -> [SizeBinder VName] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder VName -> Ident
forall vn. SizeBinder vn -> IdentBase Info vn
sizeWithType [SizeBinder VName]
sizes') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [SizeBinder VName] -> TermTypeM a
m [SizeBinder VName]
sizes'
  where
    lookForDuplicates :: Map k SrcLoc -> SizeBinder k -> m (Map k SrcLoc)
lookForDuplicates Map k SrcLoc
prev SizeBinder k
size
      | Just SrcLoc
prevloc <- k -> Map k SrcLoc -> Maybe SrcLoc
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (SizeBinder k -> k
forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) Map k SrcLoc
prev =
          SizeBinder k -> Notes -> Doc -> m (Map k SrcLoc)
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SizeBinder k
size Notes
forall a. Monoid a => a
mempty (Doc -> m (Map k SrcLoc)) -> Doc -> m (Map k SrcLoc)
forall a b. (a -> b) -> a -> b
$
            Doc
"Size name also bound at "
              Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel (SizeBinder k -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder k
size) SrcLoc
prevloc)
              Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      | Bool
otherwise =
          Map k SrcLoc -> m (Map k SrcLoc)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k SrcLoc -> m (Map k SrcLoc))
-> Map k SrcLoc -> m (Map k SrcLoc)
forall a b. (a -> b) -> a -> b
$ k -> SrcLoc -> Map k SrcLoc -> Map k SrcLoc
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (SizeBinder k -> k
forall vn. SizeBinder vn -> vn
sizeName SizeBinder k
size) (SizeBinder k -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder k
size) Map k SrcLoc
prev

    sizeWithSpace :: SizeBinder b -> (Namespace, b)
sizeWithSpace SizeBinder b
size =
      (Namespace
Term, SizeBinder b -> b
forall vn. SizeBinder vn -> vn
sizeName SizeBinder b
size)
    sizeWithType :: SizeBinder vn -> IdentBase Info vn
sizeWithType SizeBinder vn
size =
      vn
-> Info (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase Info vn
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase f vn
Ident (SizeBinder vn -> vn
forall vn. SizeBinder vn -> vn
sizeName SizeBinder vn
size) (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (PrimType -> ScalarTypeBase (DimDecl VName) Aliasing
forall dim as. PrimType -> ScalarTypeBase dim as
Prim (IntType -> PrimType
Signed IntType
Int64)))) (SizeBinder vn -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf SizeBinder vn
size)

    check :: SizeBinder Name -> f (SizeBinder VName)
check (SizeBinder Name
v SrcLoc
loc) =
      VName -> SrcLoc -> SizeBinder VName
forall vn. vn -> SrcLoc -> SizeBinder vn
SizeBinder (VName -> SrcLoc -> SizeBinder VName)
-> f VName -> f (SrcLoc -> SizeBinder VName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Namespace -> Name -> SrcLoc -> f VName
forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
loc f (SrcLoc -> SizeBinder VName) -> f SrcLoc -> f (SizeBinder VName)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> f SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc

sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam :: SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam (SizeBinder VName
v SrcLoc
loc) = Name -> SrcLoc -> UncheckedTypeParam
forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim (VName -> Name
baseName VName
v) SrcLoc
loc

-- | Check and bind a @let@-pattern.
bindingPat ::
  [SizeBinder VName] ->
  PatBase NoInfo Name ->
  InferredType ->
  (Pat -> TermTypeM a) ->
  TermTypeM a
bindingPat :: [SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
bindingPat [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t Pat -> TermTypeM a
m = do
  [UncheckedTypeParam] -> [PatBase NoInfo Name] -> TermTypeM ()
forall (m :: * -> *).
MonadTypeChecker m =>
[UncheckedTypeParam] -> [PatBase NoInfo Name] -> m ()
checkForDuplicateNames ((SizeBinder VName -> UncheckedTypeParam)
-> [SizeBinder VName] -> [UncheckedTypeParam]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam [SizeBinder VName]
sizes) [PatBase NoInfo Name
p]
  [SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
forall a.
[SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
checkPat [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t ((Pat -> TermTypeM a) -> TermTypeM a)
-> (Pat -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat
p' -> Bool -> [Ident] -> TermTypeM a -> TermTypeM a
forall a. Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
True (Set Ident -> [Ident]
forall a. Set a -> [a]
S.toList (Set Ident -> [Ident]) -> Set Ident -> [Ident]
forall a b. (a -> b) -> a -> b
$ Pat -> Set Ident
forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set (IdentBase f vn)
patIdents Pat
p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    -- Perform an observation of every declared dimension.  This
    -- prevents unused-name warnings for otherwise unused dimensions.
    let ident :: SizeBinder vn -> IdentBase Info vn
ident (SizeBinder vn
v SrcLoc
loc) =
          vn
-> Info (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase Info vn
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing)
-> SrcLoc
-> IdentBase f vn
Ident vn
v (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) Aliasing
 -> TypeBase (DimDecl VName) Aliasing)
-> ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (DimDecl VName) Aliasing
forall dim as. PrimType -> ScalarTypeBase dim as
Prim (PrimType -> ScalarTypeBase (DimDecl VName) Aliasing)
-> PrimType -> ScalarTypeBase (DimDecl VName) Aliasing
forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64)) SrcLoc
loc
    (SizeBinder VName -> TermTypeM ())
-> [SizeBinder VName] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ident -> TermTypeM ()
observe (Ident -> TermTypeM ())
-> (SizeBinder VName -> Ident) -> SizeBinder VName -> TermTypeM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> Ident
forall vn. SizeBinder vn -> IdentBase Info vn
ident) [SizeBinder VName]
sizes

    let used_sizes :: Set VName
used_sizes = StructType -> Set VName
forall als. TypeBase (DimDecl VName) als -> Set VName
typeDimNames (StructType -> Set VName) -> StructType -> Set VName
forall a b. (a -> b) -> a -> b
$ Pat -> StructType
patternStructType Pat
p'
    case (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> [SizeBinder VName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
used_sizes) (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 -> TermTypeM a
m Pat
p'
      SizeBinder VName
size : [SizeBinder VName]
_ -> SizeBinder VName -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
SizeBinder VName -> m a
unusedSize SizeBinder VName
size

-- All this complexity is just so we can handle un-suffixed numeric
-- literals in patterns.
patLitMkType :: PatLit -> SrcLoc -> TermTypeM StructType
patLitMkType :: PatLit -> SrcLoc -> TermTypeM StructType
patLitMkType (PatLitInt Integer
_) SrcLoc
loc = do
  StructType
t <- SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [PrimType] -> Usage -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyNumberType (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"integer literal") StructType
t
  StructType -> TermTypeM StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
patLitMkType (PatLitFloat Double
_) SrcLoc
loc = do
  StructType
t <- SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [PrimType] -> Usage -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
[PrimType] -> Usage -> StructType -> m ()
mustBeOneOf [PrimType]
anyFloatType (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"float literal") StructType
t
  StructType -> TermTypeM StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
patLitMkType (PatLitPrim PrimValue
v) SrcLoc
_ =
  StructType -> TermTypeM StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructType -> TermTypeM StructType)
-> StructType -> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase (DimDecl VName) () -> StructType)
-> ScalarTypeBase (DimDecl VName) () -> StructType
forall a b. (a -> b) -> a -> b
$ PrimType -> ScalarTypeBase (DimDecl VName) ()
forall dim as. PrimType -> ScalarTypeBase dim as
Prim (PrimType -> ScalarTypeBase (DimDecl VName) ())
-> PrimType -> ScalarTypeBase (DimDecl VName) ()
forall a b. (a -> b) -> a -> b
$ PrimValue -> PrimType
primValueType PrimValue
v

checkPat' ::
  [SizeBinder VName] ->
  UncheckedPat ->
  InferredType ->
  TermTypeM Pat
checkPat' :: [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes (PatParens PatBase NoInfo Name
p SrcLoc
loc) InferredType
t =
  Pat -> SrcLoc -> Pat
forall (f :: * -> *) vn. PatBase f vn -> SrcLoc -> PatBase f vn
PatParens (Pat -> SrcLoc -> Pat)
-> TermTypeM Pat -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatAttr AttrInfo Name
attr PatBase NoInfo Name
p SrcLoc
loc) InferredType
t =
  AttrInfo VName -> Pat -> SrcLoc -> Pat
forall (f :: * -> *) vn.
AttrInfo vn -> PatBase f vn -> SrcLoc -> PatBase f vn
PatAttr (AttrInfo VName -> Pat -> SrcLoc -> Pat)
-> TermTypeM (AttrInfo VName) -> TermTypeM (Pat -> SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AttrInfo Name -> TermTypeM (AttrInfo VName)
forall (m :: * -> *).
MonadTypeChecker m =>
AttrInfo Name -> m (AttrInfo VName)
checkAttr AttrInfo Name
attr TermTypeM (Pat -> SrcLoc -> Pat)
-> TermTypeM Pat -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo (TypeBase (DimDecl VName) Aliasing)
_ SrcLoc
loc) InferredType
_
  | String
name' String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
doNotShadow =
      SrcLoc -> Notes -> Doc -> TermTypeM Pat
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError SrcLoc
loc Notes
forall a. Monoid a => a
mempty (Doc -> TermTypeM Pat) -> Doc -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Doc
"The" Doc -> Doc -> Doc
<+> String -> Doc
text String
name' Doc -> Doc -> Doc
<+> Doc
"operator may not be redefined."
  where
    name' :: String
name' = Name -> String
nameToString Name
name
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) = do
  VName
name' <- Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ VName -> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
Id VName
name' (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info TypeBase (DimDecl VName) Aliasing
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Id Name
name NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
loc) InferredType
NoneInferred = do
  VName
name' <- Name -> TermTypeM VName
forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newID Name
name
  TypeBase (DimDecl VName) Aliasing
t <- SrcLoc -> Name -> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ VName -> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
vn
-> f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
Id VName
name' (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info TypeBase (DimDecl VName) Aliasing
t) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Wildcard NoInfo (TypeBase (DimDecl VName) Aliasing)
_ SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) =
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
Wildcard (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (TypeBase (DimDecl VName) Aliasing
 -> Info (TypeBase (DimDecl VName) Aliasing))
-> TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing
t TypeBase (DimDecl VName) Aliasing
-> Uniqueness -> TypeBase (DimDecl VName) Aliasing
forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (Wildcard NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
loc) InferredType
NoneInferred = do
  TypeBase (DimDecl VName) Aliasing
t <- SrcLoc -> Name -> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
Wildcard (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info TypeBase (DimDecl VName) Aliasing
t) SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (TuplePat [PatBase NoInfo Name]
ps SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t)
  | Just [TypeBase (DimDecl VName) Aliasing]
ts <- TypeBase (DimDecl VName) Aliasing
-> Maybe [TypeBase (DimDecl VName) Aliasing]
forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord TypeBase (DimDecl VName) Aliasing
t,
    [TypeBase (DimDecl VName) Aliasing] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [TypeBase (DimDecl VName) Aliasing]
ts Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== [PatBase NoInfo Name] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [PatBase NoInfo Name]
ps =
      [Pat] -> SrcLoc -> Pat
forall (f :: * -> *) vn. [PatBase f vn] -> SrcLoc -> PatBase f vn
TuplePat
        ([Pat] -> SrcLoc -> Pat)
-> TermTypeM [Pat] -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name -> InferredType -> TermTypeM Pat)
-> [PatBase NoInfo Name] -> [InferredType] -> TermTypeM [Pat]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes) [PatBase NoInfo Name]
ps ((TypeBase (DimDecl VName) Aliasing -> InferredType)
-> [TypeBase (DimDecl VName) Aliasing] -> [InferredType]
forall a b. (a -> b) -> [a] -> [b]
map TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed [TypeBase (DimDecl VName) Aliasing]
ts)
        TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes p :: PatBase NoInfo Name
p@(TuplePat [PatBase NoInfo Name]
ps SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) = do
  [StructType]
ps_t <- Level -> TermTypeM StructType -> TermTypeM [StructType]
forall (m :: * -> *) a. Applicative m => Level -> m a -> m [a]
replicateM ([PatBase NoInfo Name] -> Level
forall (t :: * -> *) a. Foldable t => t a -> Level
length [PatBase NoInfo Name]
ps) (SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t")
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"matching a tuple pattern") (ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar ([StructType] -> ScalarTypeBase (DimDecl VName) ()
forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord [StructType]
ps_t)) (StructType -> TermTypeM ()) -> StructType -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase (DimDecl VName) Aliasing
t
  TypeBase (DimDecl VName) Aliasing
t' <- TypeBase (DimDecl VName) Aliasing
-> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase (DimDecl VName) Aliasing
t
  [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p (InferredType -> TermTypeM Pat) -> InferredType -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed TypeBase (DimDecl VName) Aliasing
t'
checkPat' [SizeBinder VName]
sizes (TuplePat [PatBase NoInfo Name]
ps SrcLoc
loc) InferredType
NoneInferred =
  [Pat] -> SrcLoc -> Pat
forall (f :: * -> *) vn. [PatBase f vn] -> SrcLoc -> PatBase f vn
TuplePat ([Pat] -> SrcLoc -> Pat)
-> TermTypeM [Pat] -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name -> TermTypeM Pat)
-> [PatBase NoInfo Name] -> TermTypeM [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PatBase NoInfo Name
p -> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
NoneInferred) [PatBase NoInfo Name]
ps TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (RecordPat [(Name, PatBase NoInfo Name)]
p_fs SrcLoc
_) InferredType
_
  | Just (Name
f, PatBase NoInfo Name
fp) <- ((Name, PatBase NoInfo Name) -> Bool)
-> [(Name, PatBase NoInfo Name)]
-> Maybe (Name, PatBase NoInfo Name)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
"_" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) (String -> Bool)
-> ((Name, PatBase NoInfo Name) -> String)
-> (Name, PatBase NoInfo Name)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameToString (Name -> String)
-> ((Name, PatBase NoInfo Name) -> Name)
-> (Name, PatBase NoInfo Name)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, PatBase NoInfo Name) -> Name
forall a b. (a, b) -> a
fst) [(Name, PatBase NoInfo Name)]
p_fs =
      PatBase NoInfo Name -> Notes -> Doc -> TermTypeM Pat
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc -> m a
typeError PatBase NoInfo Name
fp Notes
forall a. Monoid a => a
mempty (Doc -> TermTypeM Pat) -> Doc -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$
        Doc
"Underscore-prefixed fields are not allowed."
          Doc -> Doc -> Doc
</> Doc
"Did you mean" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
dquotes (String -> Doc
text (Level -> String -> String
forall a. Level -> [a] -> [a]
drop Level
1 (Name -> String
nameToString Name
f)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"=_") Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"?"
checkPat' [SizeBinder VName]
sizes (RecordPat [(Name, PatBase NoInfo Name)]
p_fs SrcLoc
loc) (Ascribed (Scalar (Record Map Name (TypeBase (DimDecl VName) Aliasing)
t_fs)))
  | [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (((Name, PatBase NoInfo Name) -> Name)
-> [(Name, PatBase NoInfo Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase NoInfo Name) -> Name
forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name)]
p_fs) [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (Map Name (TypeBase (DimDecl VName) Aliasing) -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name (TypeBase (DimDecl VName) Aliasing)
t_fs) =
      [(Name, Pat)] -> SrcLoc -> Pat
forall (f :: * -> *) vn.
[(Name, PatBase f vn)] -> SrcLoc -> PatBase f vn
RecordPat ([(Name, Pat)] -> SrcLoc -> Pat)
-> (Map Name Pat -> [(Name, Pat)]) -> Map Name Pat -> SrcLoc -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name Pat -> [(Name, Pat)]
forall k a. Map k a -> [(k, a)]
M.toList (Map Name Pat -> SrcLoc -> Pat)
-> TermTypeM (Map Name Pat) -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermTypeM (Map Name Pat)
check TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
  where
    check :: TermTypeM (Map Name Pat)
check =
      ((PatBase NoInfo Name, InferredType) -> TermTypeM Pat)
-> Map Name (PatBase NoInfo Name, InferredType)
-> TermTypeM (Map Name Pat)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((PatBase NoInfo Name -> InferredType -> TermTypeM Pat)
-> (PatBase NoInfo Name, InferredType) -> TermTypeM Pat
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes)) (Map Name (PatBase NoInfo Name, InferredType)
 -> TermTypeM (Map Name Pat))
-> Map Name (PatBase NoInfo Name, InferredType)
-> TermTypeM (Map Name Pat)
forall a b. (a -> b) -> a -> b
$
        (PatBase NoInfo Name
 -> InferredType -> (PatBase NoInfo Name, InferredType))
-> Map Name (PatBase NoInfo Name)
-> Map Name InferredType
-> Map Name (PatBase NoInfo Name, InferredType)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) ([(Name, PatBase NoInfo Name)] -> Map Name (PatBase NoInfo Name)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name)]
p_fs) ((TypeBase (DimDecl VName) Aliasing -> InferredType)
-> Map Name (TypeBase (DimDecl VName) Aliasing)
-> Map Name InferredType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed Map Name (TypeBase (DimDecl VName) Aliasing)
t_fs)
checkPat' [SizeBinder VName]
sizes p :: PatBase NoInfo Name
p@(RecordPat [(Name, PatBase NoInfo Name)]
fields SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) = do
  Map Name StructType
fields' <- (PatBase NoInfo Name -> TermTypeM StructType)
-> Map Name (PatBase NoInfo Name)
-> TermTypeM (Map Name StructType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TermTypeM StructType -> PatBase NoInfo Name -> TermTypeM StructType
forall a b. a -> b -> a
const (TermTypeM StructType
 -> PatBase NoInfo Name -> TermTypeM StructType)
-> TermTypeM StructType
-> PatBase NoInfo Name
-> TermTypeM StructType
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t") (Map Name (PatBase NoInfo Name) -> TermTypeM (Map Name StructType))
-> Map Name (PatBase NoInfo Name)
-> TermTypeM (Map Name StructType)
forall a b. (a -> b) -> a -> b
$ [(Name, PatBase NoInfo Name)] -> Map Name (PatBase NoInfo Name)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name)]
fields

  Bool -> TermTypeM () -> TermTypeM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (Map Name StructType -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name StructType
fields') [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Name] -> [Name]
forall a. Ord a => [a] -> [a]
sort (((Name, PatBase NoInfo Name) -> Name)
-> [(Name, PatBase NoInfo Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PatBase NoInfo Name) -> Name
forall a b. (a, b) -> a
fst [(Name, PatBase NoInfo Name)]
fields)) (TermTypeM () -> TermTypeM ()) -> TermTypeM () -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$
    SrcLoc -> Notes -> Doc -> TermTypeM ()
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
<+> PatBase NoInfo Name -> Doc
forall a. Pretty a => a -> Doc
ppr PatBase NoInfo Name
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 -> String -> Usage
mkUsage SrcLoc
loc String
"matching a record pattern") (ScalarTypeBase (DimDecl VName) () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (Map Name StructType -> ScalarTypeBase (DimDecl VName) ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
fields')) (StructType -> TermTypeM ()) -> StructType -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase (DimDecl VName) Aliasing
t
  TypeBase (DimDecl VName) Aliasing
t' <- TypeBase (DimDecl VName) Aliasing
-> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase (DimDecl VName) Aliasing
t
  [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p (InferredType -> TermTypeM Pat) -> InferredType -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed TypeBase (DimDecl VName) Aliasing
t'
checkPat' [SizeBinder VName]
sizes (RecordPat [(Name, PatBase NoInfo Name)]
fs SrcLoc
loc) InferredType
NoneInferred =
  [(Name, Pat)] -> SrcLoc -> Pat
forall (f :: * -> *) vn.
[(Name, PatBase f vn)] -> SrcLoc -> PatBase f vn
RecordPat ([(Name, Pat)] -> SrcLoc -> Pat)
-> (Map Name Pat -> [(Name, Pat)]) -> Map Name Pat -> SrcLoc -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name Pat -> [(Name, Pat)]
forall k a. Map k a -> [(k, a)]
M.toList
    (Map Name Pat -> SrcLoc -> Pat)
-> TermTypeM (Map Name Pat) -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PatBase NoInfo Name -> TermTypeM Pat)
-> Map Name (PatBase NoInfo Name) -> TermTypeM (Map Name Pat)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\PatBase NoInfo Name
p -> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
NoneInferred) ([(Name, PatBase NoInfo Name)] -> Map Name (PatBase NoInfo Name)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase NoInfo Name)]
fs)
    TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatAscription PatBase NoInfo Name
p TypeExp Name
t SrcLoc
loc) InferredType
maybe_outer_t = do
  (TypeExp VName
t', StructType
st, [VName]
_) <- TypeExp Name -> TermTypeM (TypeExp VName, StructType, [VName])
checkTypeExpNonrigid TypeExp Name
t

  case InferredType
maybe_outer_t of
    Ascribed TypeBase (DimDecl VName) Aliasing
outer_t -> do
      StructType
st_forunify <- [SizeBinder VName] -> StructType -> TermTypeM StructType
nonrigidFor [SizeBinder VName]
sizes StructType
st
      Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"explicit type ascription") StructType
st_forunify (TypeBase (DimDecl VName) Aliasing -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase (DimDecl VName) Aliasing
outer_t)

      TypeBase (DimDecl VName) Aliasing
outer_t' <- TypeBase (DimDecl VName) Aliasing
-> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase (DimDecl VName) Aliasing
outer_t
      Pat -> TypeExp VName -> SrcLoc -> Pat
forall (f :: * -> *) vn.
PatBase f vn -> TypeExp vn -> SrcLoc -> PatBase f vn
PatAscription
        (Pat -> TypeExp VName -> SrcLoc -> Pat)
-> TermTypeM Pat -> TermTypeM (TypeExp VName -> SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p (TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed (StructType
-> TypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
addAliasesFromType StructType
st TypeBase (DimDecl VName) Aliasing
outer_t'))
        TermTypeM (TypeExp VName -> SrcLoc -> Pat)
-> TermTypeM (TypeExp VName) -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp VName -> TermTypeM (TypeExp VName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp VName
t'
        TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
    InferredType
NoneInferred ->
      Pat -> TypeExp VName -> SrcLoc -> Pat
forall (f :: * -> *) vn.
PatBase f vn -> TypeExp vn -> SrcLoc -> PatBase f vn
PatAscription (Pat -> TypeExp VName -> SrcLoc -> Pat)
-> TermTypeM Pat -> TermTypeM (TypeExp VName -> SrcLoc -> Pat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p (TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed (StructType -> TypeBase (DimDecl VName) Aliasing
forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
st))
        TermTypeM (TypeExp VName -> SrcLoc -> Pat)
-> TermTypeM (TypeExp VName) -> TermTypeM (SrcLoc -> Pat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeExp VName -> TermTypeM (TypeExp VName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeExp VName
t'
        TermTypeM (SrcLoc -> Pat) -> TermTypeM SrcLoc -> TermTypeM Pat
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SrcLoc -> TermTypeM SrcLoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
checkPat' [SizeBinder VName]
_ (PatLit PatLit
l NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) = do
  StructType
t' <- PatLit -> SrcLoc -> TermTypeM StructType
patLitMkType PatLit
l SrcLoc
loc
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify (SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"matching against literal") StructType
t' (TypeBase (DimDecl VName) Aliasing -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase (DimDecl VName) Aliasing
t)
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ PatLit -> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
PatLit
-> f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
PatLit PatLit
l (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (StructType -> TypeBase (DimDecl VName) Aliasing
forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
t')) SrcLoc
loc
checkPat' [SizeBinder VName]
_ (PatLit PatLit
l NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo SrcLoc
loc) InferredType
NoneInferred = do
  StructType
t' <- PatLit -> SrcLoc -> TermTypeM StructType
patLitMkType PatLit
l SrcLoc
loc
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ PatLit -> Info (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> Pat
forall (f :: * -> *) vn.
PatLit
-> f (TypeBase (DimDecl VName) Aliasing) -> SrcLoc -> PatBase f vn
PatLit PatLit
l (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (StructType -> TypeBase (DimDecl VName) Aliasing
forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
t')) SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo [PatBase NoInfo Name]
ps SrcLoc
loc) (Ascribed (Scalar (Sum Map Name [TypeBase (DimDecl VName) Aliasing]
cs)))
  | Just [TypeBase (DimDecl VName) Aliasing]
ts <- Name
-> Map Name [TypeBase (DimDecl VName) Aliasing]
-> Maybe [TypeBase (DimDecl VName) Aliasing]
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name [TypeBase (DimDecl VName) Aliasing]
cs = do
      [Pat]
ps' <- (PatBase NoInfo Name -> InferredType -> TermTypeM Pat)
-> [PatBase NoInfo Name] -> [InferredType] -> TermTypeM [Pat]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes) [PatBase NoInfo Name]
ps ([InferredType] -> TermTypeM [Pat])
-> [InferredType] -> TermTypeM [Pat]
forall a b. (a -> b) -> a -> b
$ (TypeBase (DimDecl VName) Aliasing -> InferredType)
-> [TypeBase (DimDecl VName) Aliasing] -> [InferredType]
forall a b. (a -> b) -> [a] -> [b]
map TypeBase (DimDecl VName) Aliasing -> InferredType
Ascribed [TypeBase (DimDecl VName) Aliasing]
ts
      Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Name
-> Info (TypeBase (DimDecl VName) Aliasing)
-> [Pat]
-> SrcLoc
-> Pat
forall (f :: * -> *) vn.
Name
-> f (TypeBase (DimDecl VName) Aliasing)
-> [PatBase f vn]
-> SrcLoc
-> PatBase f vn
PatConstr Name
n (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (ScalarTypeBase (DimDecl VName) Aliasing
-> TypeBase (DimDecl VName) Aliasing
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (Map Name [TypeBase (DimDecl VName) Aliasing]
-> ScalarTypeBase (DimDecl VName) Aliasing
forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum Map Name [TypeBase (DimDecl VName) Aliasing]
cs))) [Pat]
ps' SrcLoc
loc
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo [PatBase NoInfo Name]
ps SrcLoc
loc) (Ascribed TypeBase (DimDecl VName) Aliasing
t) = do
  StructType
t' <- SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  [Pat]
ps' <- (PatBase NoInfo Name -> TermTypeM Pat)
-> [PatBase NoInfo Name] -> TermTypeM [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PatBase NoInfo Name
p -> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
NoneInferred) [PatBase NoInfo Name]
ps
  Usage -> Name -> StructType -> [StructType] -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n StructType
t' (Pat -> StructType
patternStructType (Pat -> StructType) -> [Pat] -> [StructType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat]
ps')
  Usage -> StructType -> StructType -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
t' (TypeBase (DimDecl VName) Aliasing -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase (DimDecl VName) Aliasing
t)
  TypeBase (DimDecl VName) Aliasing
t'' <- TypeBase (DimDecl VName) Aliasing
-> TermTypeM (TypeBase (DimDecl VName) Aliasing)
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully TypeBase (DimDecl VName) Aliasing
t
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Name
-> Info (TypeBase (DimDecl VName) Aliasing)
-> [Pat]
-> SrcLoc
-> Pat
forall (f :: * -> *) vn.
Name
-> f (TypeBase (DimDecl VName) Aliasing)
-> [PatBase f vn]
-> SrcLoc
-> PatBase f vn
PatConstr Name
n (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info TypeBase (DimDecl VName) Aliasing
t'') [Pat]
ps' SrcLoc
loc
  where
    usage :: Usage
usage = SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"matching against constructor"
checkPat' [SizeBinder VName]
sizes (PatConstr Name
n NoInfo (TypeBase (DimDecl VName) Aliasing)
NoInfo [PatBase NoInfo Name]
ps SrcLoc
loc) InferredType
NoneInferred = do
  [Pat]
ps' <- (PatBase NoInfo Name -> TermTypeM Pat)
-> [PatBase NoInfo Name] -> TermTypeM [Pat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PatBase NoInfo Name
p -> [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
NoneInferred) [PatBase NoInfo Name]
ps
  StructType
t <- SrcLoc -> Name -> TermTypeM StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar SrcLoc
loc Name
"t"
  Usage -> Name -> StructType -> [StructType] -> TermTypeM ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> Name -> StructType -> [StructType] -> m ()
mustHaveConstr Usage
usage Name
n StructType
t (Pat -> StructType
patternStructType (Pat -> StructType) -> [Pat] -> [StructType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pat]
ps')
  Pat -> TermTypeM Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> TermTypeM Pat) -> Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ Name
-> Info (TypeBase (DimDecl VName) Aliasing)
-> [Pat]
-> SrcLoc
-> Pat
forall (f :: * -> *) vn.
Name
-> f (TypeBase (DimDecl VName) Aliasing)
-> [PatBase f vn]
-> SrcLoc
-> PatBase f vn
PatConstr Name
n (TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a. a -> Info a
Info (TypeBase (DimDecl VName) Aliasing
 -> Info (TypeBase (DimDecl VName) Aliasing))
-> TypeBase (DimDecl VName) Aliasing
-> Info (TypeBase (DimDecl VName) Aliasing)
forall a b. (a -> b) -> a -> b
$ StructType -> TypeBase (DimDecl VName) Aliasing
forall dim as. TypeBase dim as -> TypeBase dim Aliasing
fromStruct StructType
t) [Pat]
ps' SrcLoc
loc
  where
    usage :: Usage
usage = SrcLoc -> String -> Usage
mkUsage SrcLoc
loc String
"matching against constructor"

patNameMap :: Pat -> NameMap
patNameMap :: Pat -> NameMap
patNameMap = [((Namespace, Name), QualName VName)] -> NameMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([((Namespace, Name), QualName VName)] -> NameMap)
-> (Pat -> [((Namespace, Name), QualName VName)]) -> Pat -> NameMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VName -> ((Namespace, Name), QualName VName))
-> [VName] -> [((Namespace, Name), QualName VName)]
forall a b. (a -> b) -> [a] -> [b]
map VName -> ((Namespace, Name), QualName VName)
asTerm ([VName] -> [((Namespace, Name), QualName VName)])
-> (Pat -> [VName]) -> Pat -> [((Namespace, Name), QualName VName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set VName -> [VName]
forall a. Set a -> [a]
S.toList (Set VName -> [VName]) -> (Pat -> Set VName) -> Pat -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat -> Set VName
forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames
  where
    asTerm :: VName -> ((Namespace, Name), QualName VName)
asTerm VName
v = ((Namespace
Term, VName -> Name
baseName VName
v), VName -> QualName VName
forall v. v -> QualName v
qualName VName
v)

checkPat ::
  [SizeBinder VName] ->
  UncheckedPat ->
  InferredType ->
  (Pat -> TermTypeM a) ->
  TermTypeM a
checkPat :: [SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
checkPat [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t Pat -> TermTypeM a
m = do
  [UncheckedTypeParam] -> [PatBase NoInfo Name] -> TermTypeM ()
forall (m :: * -> *).
MonadTypeChecker m =>
[UncheckedTypeParam] -> [PatBase NoInfo Name] -> m ()
checkForDuplicateNames ((SizeBinder VName -> UncheckedTypeParam)
-> [SizeBinder VName] -> [UncheckedTypeParam]
forall a b. (a -> b) -> [a] -> [b]
map SizeBinder VName -> UncheckedTypeParam
sizeBinderToParam [SizeBinder VName]
sizes) [PatBase NoInfo Name
p]
  Pat
p' <- Checking -> TermTypeM Pat -> TermTypeM Pat
forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (PatBase NoInfo Name -> InferredType -> Checking
CheckingPat PatBase NoInfo Name
p InferredType
t) (TermTypeM Pat -> TermTypeM Pat) -> TermTypeM Pat -> TermTypeM Pat
forall a b. (a -> b) -> a -> b
$ [SizeBinder VName]
-> PatBase NoInfo Name -> InferredType -> TermTypeM Pat
checkPat' [SizeBinder VName]
sizes PatBase NoInfo Name
p InferredType
t

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

  case (SizeBinder VName -> Bool)
-> [SizeBinder VName] -> [SizeBinder VName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VName -> Set VName -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
explicit) (VName -> Bool)
-> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeBinder VName -> VName
forall vn. SizeBinder vn -> vn
sizeName) [SizeBinder VName]
sizes of
    SizeBinder VName
size : [SizeBinder VName]
_ ->
      SizeBinder VName -> Notes -> Doc -> TermTypeM a
forall (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
<+> SizeBinder VName -> Doc
forall a. Pretty a => a -> Doc
ppr SizeBinder VName
size
          Doc -> Doc -> Doc
<+> Doc
"as it is never used as the size of a concrete (non-function) value."
    [] ->
      NameMap -> TermTypeM a -> TermTypeM a
forall (m :: * -> *) a. MonadTypeChecker m => NameMap -> m a -> m a
bindNameMap (Pat -> NameMap
patNameMap Pat
p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ Pat -> TermTypeM a
m Pat
p'

-- | Check and bind type and value parameters.
bindingParams ::
  [UncheckedTypeParam] ->
  [UncheckedPat] ->
  ([TypeParam] -> [Pat] -> TermTypeM a) ->
  TermTypeM a
bindingParams :: [UncheckedTypeParam]
-> [PatBase NoInfo Name]
-> ([TypeParam] -> [Pat] -> TermTypeM a)
-> TermTypeM a
bindingParams [UncheckedTypeParam]
tps [PatBase NoInfo Name]
orig_ps [TypeParam] -> [Pat] -> TermTypeM a
m = do
  [UncheckedTypeParam] -> [PatBase NoInfo Name] -> TermTypeM ()
forall (m :: * -> *).
MonadTypeChecker m =>
[UncheckedTypeParam] -> [PatBase NoInfo Name] -> m ()
checkForDuplicateNames [UncheckedTypeParam]
tps [PatBase NoInfo Name]
orig_ps
  [UncheckedTypeParam] -> ([TypeParam] -> TermTypeM a) -> TermTypeM a
forall (m :: * -> *) a.
MonadTypeChecker m =>
[UncheckedTypeParam] -> ([TypeParam] -> m a) -> m a
checkTypeParams [UncheckedTypeParam]
tps (([TypeParam] -> TermTypeM a) -> TermTypeM a)
-> ([TypeParam] -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \[TypeParam]
tps' -> [TypeParam] -> TermTypeM a -> TermTypeM a
forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
bindingTypeParams [TypeParam]
tps' (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ do
    let descend :: [Pat] -> [PatBase NoInfo Name] -> TermTypeM a
descend [Pat]
ps' (PatBase NoInfo Name
p : [PatBase NoInfo Name]
ps) =
          [SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
forall a.
[SizeBinder VName]
-> PatBase NoInfo Name
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
checkPat [] PatBase NoInfo Name
p InferredType
NoneInferred ((Pat -> TermTypeM a) -> TermTypeM a)
-> (Pat -> TermTypeM a) -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ \Pat
p' ->
            Bool -> [Ident] -> TermTypeM a -> TermTypeM a
forall a. Bool -> [Ident] -> TermTypeM a -> TermTypeM a
binding Bool
False (Set Ident -> [Ident]
forall a. Set a -> [a]
S.toList (Set Ident -> [Ident]) -> Set Ident -> [Ident]
forall a b. (a -> b) -> a -> b
$ Pat -> Set Ident
forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set (IdentBase f vn)
patIdents Pat
p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat] -> [PatBase NoInfo Name] -> TermTypeM a
descend (Pat
p' Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
ps') [PatBase NoInfo Name]
ps
        descend [Pat]
ps' [] = do
          -- Perform an observation of every type parameter.  This
          -- prevents unused-name warnings for otherwise unused
          -- dimensions.
          (Ident -> TermTypeM ()) -> [Ident] -> TermTypeM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Ident -> TermTypeM ()
observe ([Ident] -> TermTypeM ()) -> [Ident] -> TermTypeM ()
forall a b. (a -> b) -> a -> b
$ (TypeParam -> Maybe Ident) -> [TypeParam] -> [Ident]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TypeParam -> Maybe Ident
typeParamIdent [TypeParam]
tps'
          [TypeParam] -> [Pat] -> TermTypeM a
m [TypeParam]
tps' ([Pat] -> TermTypeM a) -> [Pat] -> TermTypeM a
forall a b. (a -> b) -> a -> b
$ [Pat] -> [Pat]
forall a. [a] -> [a]
reverse [Pat]
ps'

    [Pat] -> [PatBase NoInfo Name] -> TermTypeM a
descend [] [PatBase NoInfo Name]
orig_ps