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

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

    nonrigidFor :: [(SizeBinder VName, QualName VName)] -> StructType -> StructType
    nonrigidFor :: [(SizeBinder VName, QualName VName)] -> StructType -> StructType
    nonrigidFor [] = StructType -> StructType
    forall a. a -> a
    id -- Minor optimisation.
    nonrigidFor [(SizeBinder VName, QualName VName)]
    sizes = (ExpBase Info VName -> ExpBase Info VName)
    -> StructType -> StructType
    forall a b c. (a -> b) -> TypeBase a c -> TypeBase b c
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first ExpBase Info VName -> ExpBase Info VName
    forall {f :: * -> *}. ExpBase f VName -> ExpBase f VName
    onDim
      where
        onDim :: ExpBase f VName -> ExpBase f VName
    onDim (Var (QualName [VName]
    _ VName
    v) f StructType
    info SrcLoc
    loc)
          | Just (SizeBinder VName
    _, QualName VName
    v') <- ((SizeBinder VName, QualName VName) -> Bool)
    -> [(SizeBinder VName, QualName VName)]
    -> Maybe (SizeBinder VName, QualName VName)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find ((VName -> VName -> Bool
    forall a. Eq a => a -> a -> Bool
    == VName
    v) (VName -> Bool)
    -> ((SizeBinder VName, QualName VName) -> VName)
    -> (SizeBinder VName, QualName VName)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeBinder VName -> VName
    forall vn. SizeBinder vn -> vn
    sizeName (SizeBinder VName -> VName)
    -> ((SizeBinder VName, QualName VName) -> SizeBinder VName)
    -> (SizeBinder VName, QualName VName)
    -> VName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SizeBinder VName, QualName VName) -> SizeBinder VName
    forall a b. (a, b) -> a
    fst) [(SizeBinder VName, QualName VName)]
    sizes =
              QualName VName -> f StructType -> SrcLoc -> ExpBase f VName
    forall (f :: * -> *) vn.
    QualName vn -> f StructType -> SrcLoc -> ExpBase f vn
    Var QualName VName
    v' f StructType
    info SrcLoc
    loc
        onDim ExpBase f VName
    d = ExpBase f VName
    d

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

        bindVar :: TermScope -> Ident StructType -> TermScope
    bindVar TermScope
    scope (Ident VName
    name (Info StructType
    tp) SrcLoc
    _) =
          TermScope
    scope
            { scopeVtable =
                M.insert name (BoundV [] tp) $ scopeVtable scope
            }

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

    bindingTypeParams :: [TypeParam] -> TermTypeM a -> TermTypeM a
    bindingTypeParams :: forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
    bindingTypeParams [TypeParam]
    tparams =
      [Ident StructType] -> TermTypeM a -> TermTypeM a
    forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
    binding ((TypeParam -> Maybe (Ident StructType))
    -> [TypeParam] -> [Ident StructType]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TypeParam -> Maybe (Ident StructType)
    typeParamIdent [TypeParam]
    tparams)
        (TermTypeM a -> TermTypeM a)
    -> (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Either (VName, TypeBinding) (VName, Constraint)]
    -> TermTypeM a -> TermTypeM a
    forall a.
    [Either (VName, TypeBinding) (VName, Constraint)]
    -> TermTypeM a -> TermTypeM a
    bindingTypes ((TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)])
    -> [TypeParam] -> [Either (VName, TypeBinding) (VName, Constraint)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)]
    typeParamType [TypeParam]
    tparams)
      where
        typeParamType :: TypeParam -> [Either (VName, TypeBinding) (VName, Constraint)]
    typeParamType (TypeParamType Liftedness
    l VName
    v SrcLoc
    loc) =
          [ (VName, TypeBinding)
    -> Either (VName, TypeBinding) (VName, Constraint)
    forall a b. a -> Either a b
    Left (VName
    v, Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
    TypeAbbr Liftedness
    l [] (StructRetType -> TypeBinding) -> StructRetType -> TypeBinding
    forall a b. (a -> b) -> a -> b
    $ [VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType [] (StructType -> StructRetType) -> StructType -> StructRetType
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (NoUniqueness
    -> QualName VName
    -> [TypeArg (ExpBase Info VName)]
    -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim u.
    u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
    TypeVar NoUniqueness
    forall a. Monoid a => a
    mempty (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    v) [])),
            (VName, Constraint)
    -> Either (VName, TypeBinding) (VName, Constraint)
    forall a b. b -> Either a b
    Right (VName
    v, Liftedness -> Loc -> Constraint
    ParamType Liftedness
    l (Loc -> Constraint) -> Loc -> Constraint
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc)
          ]
        typeParamType (TypeParamDim VName
    v SrcLoc
    loc) =
          [(VName, Constraint)
    -> Either (VName, TypeBinding) (VName, Constraint)
    forall a b. b -> Either a b
    Right (VName
    v, Loc -> Constraint
    ParamSize (Loc -> Constraint) -> Loc -> Constraint
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc)]

    typeParamIdent :: TypeParam -> Maybe (Ident StructType)
    typeParamIdent :: TypeParam -> Maybe (Ident StructType)
    typeParamIdent (TypeParamDim VName
    v SrcLoc
    loc) =
      Ident StructType -> Maybe (Ident StructType)
    forall a. a -> Maybe a
    Just (Ident StructType -> Maybe (Ident StructType))
    -> Ident StructType -> Maybe (Ident StructType)
    forall a b. (a -> b) -> a -> b
    $ VName -> Info StructType -> SrcLoc -> Ident StructType
    forall {k} (f :: k -> *) vn (t :: k).
    vn -> f t -> SrcLoc -> IdentBase f vn t
    Ident VName
    v (StructType -> Info StructType
    forall a. a -> Info a
    Info (StructType -> Info StructType) -> StructType -> Info StructType
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType)
    -> ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim u. PrimType -> ScalarTypeBase dim u
    Prim (PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness)
    -> PrimType -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall a b. (a -> b) -> a -> b
    $ IntType -> PrimType
    Signed IntType
    Int64) SrcLoc
    loc
    typeParamIdent TypeParam
    _ = Maybe (Ident StructType)
    forall a. Maybe a
    Nothing

    -- | Bind @let@-bound sizes.  This is usually followed by 'bindingPat'
    -- immediately afterwards.
    bindingSizes :: [SizeBinder VName] -> TermTypeM a -> TermTypeM a
    bindingSizes :: forall a. [SizeBinder VName] -> TermTypeM a -> TermTypeM a
    bindingSizes [] TermTypeM a
    m = TermTypeM a
    m -- Minor optimisation.
    bindingSizes [SizeBinder VName]
    sizes TermTypeM a
    m = [Ident StructType] -> TermTypeM a -> TermTypeM a
    forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
    binding ((SizeBinder VName -> Ident StructType)
    -> [SizeBinder VName] -> [Ident StructType]
    forall a b. (a -> b) -> [a] -> [b]
    map SizeBinder VName -> Ident StructType
    forall {vn} {dim} {u}.
    SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
    sizeWithType [SizeBinder VName]
    sizes) TermTypeM a
    m
      where
        sizeWithType :: SizeBinder vn -> IdentBase Info vn (TypeBase dim u)
    sizeWithType SizeBinder vn
    size =
          vn
    -> Info (TypeBase dim u)
    -> SrcLoc
    -> IdentBase Info vn (TypeBase dim u)
    forall {k} (f :: k -> *) vn (t :: k).
    vn -> f t -> SrcLoc -> IdentBase f vn t
    Ident (SizeBinder vn -> vn
    forall vn. SizeBinder vn -> vn
    sizeName SizeBinder vn
    size) (TypeBase dim u -> Info (TypeBase dim u)
    forall a. a -> Info a
    Info (ScalarTypeBase dim u -> TypeBase dim u
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (PrimType -> ScalarTypeBase dim u
    forall dim u. PrimType -> ScalarTypeBase dim u
    Prim (IntType -> PrimType
    Signed IntType
    Int64)))) (SizeBinder vn -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf SizeBinder vn
    size)

    -- | Bind a single term-level identifier.
    bindingIdent ::
      IdentBase NoInfo VName StructType ->
      StructType ->
      (Ident StructType -> TermTypeM a) ->
      TermTypeM a
    bindingIdent :: forall a.
    IdentBase NoInfo VName StructType
    -> StructType -> (Ident StructType -> TermTypeM a) -> TermTypeM a
    bindingIdent (Ident VName
    v NoInfo StructType
    NoInfo SrcLoc
    vloc) StructType
    t Ident StructType -> TermTypeM a
    m = do
      let ident :: Ident StructType
    ident = VName -> Info StructType -> SrcLoc -> Ident StructType
    forall {k} (f :: k -> *) vn (t :: k).
    vn -> f t -> SrcLoc -> IdentBase f vn t
    Ident VName
    v (StructType -> Info StructType
    forall a. a -> Info a
    Info StructType
    t) SrcLoc
    vloc
      [Ident StructType] -> TermTypeM a -> TermTypeM a
    forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
    binding [Ident StructType
    ident] (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ Ident StructType -> TermTypeM a
    m Ident StructType
    ident

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

    checkPat' ::
      [(SizeBinder VName, QualName VName)] ->
      PatBase NoInfo VName ParamType ->
      Inferred ParamType ->
      TermTypeM (Pat ParamType)
    checkPat' :: [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes (PatParens PatBase NoInfo VName ParamType
    p SrcLoc
    loc) Inferred ParamType
    t =
      Pat ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    PatBase f vn t -> SrcLoc -> PatBase f vn t
    PatParens (Pat ParamType -> SrcLoc -> Pat ParamType)
    -> TermTypeM (Pat ParamType) -> TermTypeM (SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p Inferred ParamType
    t TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes (PatAttr AttrInfo VName
    attr PatBase NoInfo VName ParamType
    p SrcLoc
    loc) Inferred ParamType
    t =
      AttrInfo VName -> Pat ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    AttrInfo vn -> PatBase f vn t -> SrcLoc -> PatBase f vn t
    PatAttr (AttrInfo VName -> Pat ParamType -> SrcLoc -> Pat ParamType)
    -> TermTypeM (AttrInfo VName)
    -> TermTypeM (Pat ParamType -> SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AttrInfo VName -> TermTypeM (AttrInfo VName)
    forall (m :: * -> *).
    MonadTypeChecker m =>
    AttrInfo VName -> m (AttrInfo VName)
    checkAttr AttrInfo VName
    attr TermTypeM (Pat ParamType -> SrcLoc -> Pat ParamType)
    -> TermTypeM (Pat ParamType) -> TermTypeM (SrcLoc -> Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p Inferred ParamType
    t TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    _ (Id VName
    name NoInfo ParamType
    NoInfo SrcLoc
    loc) (Ascribed ParamType
    t) =
      Pat ParamType -> TermTypeM (Pat ParamType)
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pat ParamType -> TermTypeM (Pat ParamType))
    -> Pat ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ VName -> Info ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
    Id VName
    name (ParamType -> Info ParamType
    forall a. a -> Info a
    Info ParamType
    t) SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    _ (Id VName
    name NoInfo ParamType
    NoInfo SrcLoc
    loc) Inferred ParamType
    NoneInferred = do
      ParamType
    t <- SrcLoc -> Name -> TermTypeM ParamType
    forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> TermTypeM (TypeBase dim als)
    forall (m :: * -> *) als a dim.
    (MonadUnify m, Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    newTypeVar SrcLoc
    loc Name
    "t"
      Pat ParamType -> TermTypeM (Pat ParamType)
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pat ParamType -> TermTypeM (Pat ParamType))
    -> Pat ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ VName -> Info ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t. vn -> f t -> SrcLoc -> PatBase f vn t
    Id VName
    name (ParamType -> Info ParamType
    forall a. a -> Info a
    Info ParamType
    t) SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    _ (Wildcard NoInfo ParamType
    _ SrcLoc
    loc) (Ascribed ParamType
    t) =
      Pat ParamType -> TermTypeM (Pat ParamType)
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pat ParamType -> TermTypeM (Pat ParamType))
    -> Pat ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ Info ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
    Wildcard (ParamType -> Info ParamType
    forall a. a -> Info a
    Info ParamType
    t) SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    _ (Wildcard NoInfo ParamType
    NoInfo SrcLoc
    loc) Inferred ParamType
    NoneInferred = do
      ParamType
    t <- SrcLoc -> Name -> TermTypeM ParamType
    forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> TermTypeM (TypeBase dim als)
    forall (m :: * -> *) als a dim.
    (MonadUnify m, Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    newTypeVar SrcLoc
    loc Name
    "t"
      Pat ParamType -> TermTypeM (Pat ParamType)
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pat ParamType -> TermTypeM (Pat ParamType))
    -> Pat ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ Info ParamType -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t. f t -> SrcLoc -> PatBase f vn t
    Wildcard (ParamType -> Info ParamType
    forall a. a -> Info a
    Info ParamType
    t) SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes p :: PatBase NoInfo VName ParamType
    p@(TuplePat [PatBase NoInfo VName ParamType]
    ps SrcLoc
    loc) (Ascribed ParamType
    t)
      | Just [ParamType]
    ts <- ParamType -> Maybe [ParamType]
    forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
    isTupleRecord ParamType
    t,
        [ParamType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ParamType]
    ts Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [PatBase NoInfo VName ParamType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [PatBase NoInfo VName ParamType]
    ps =
          [Pat ParamType] -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    [PatBase f vn t] -> SrcLoc -> PatBase f vn t
    TuplePat
            ([Pat ParamType] -> SrcLoc -> Pat ParamType)
    -> TermTypeM [Pat ParamType] -> TermTypeM (SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (PatBase NoInfo VName ParamType
     -> Inferred ParamType -> TermTypeM (Pat ParamType))
    -> [PatBase NoInfo VName ParamType]
    -> [Inferred ParamType]
    -> TermTypeM [Pat ParamType]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM ([(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes) [PatBase NoInfo VName ParamType]
    ps ((ParamType -> Inferred ParamType)
    -> [ParamType] -> [Inferred ParamType]
    forall a b. (a -> b) -> [a] -> [b]
    map ParamType -> Inferred ParamType
    forall t. t -> Inferred t
    Ascribed [ParamType]
    ts)
            TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
      | Bool
    otherwise = do
          [StructType]
    ps_t <- Int -> TermTypeM StructType -> TermTypeM [StructType]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM ([PatBase NoInfo VName ParamType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [PatBase NoInfo VName ParamType]
    ps) (SrcLoc -> Name -> TermTypeM StructType
    forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> TermTypeM (TypeBase dim als)
    forall (m :: * -> *) als a dim.
    (MonadUnify m, Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    newTypeVar SrcLoc
    loc Name
    "t")
          Usage -> StructType -> StructType -> TermTypeM ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify (SrcLoc -> Text -> Usage
    forall a. Located a => a -> Text -> Usage
    mkUsage SrcLoc
    loc Text
    "matching a tuple pattern") (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar ([StructType] -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
    tupleRecord [StructType]
    ps_t)) (ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct ParamType
    t)
          [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p (Inferred ParamType -> TermTypeM (Pat ParamType))
    -> Inferred ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ ParamType -> Inferred ParamType
    forall t. t -> Inferred t
    Ascribed (ParamType -> Inferred ParamType)
    -> ParamType -> Inferred ParamType
    forall a b. (a -> b) -> a -> b
    $ Diet -> StructType -> ParamType
    forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
    toParam Diet
    Observe (StructType -> ParamType) -> StructType -> ParamType
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType)
    -> ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ [StructType] -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
    tupleRecord [StructType]
    ps_t
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes (TuplePat [PatBase NoInfo VName ParamType]
    ps SrcLoc
    loc) Inferred ParamType
    NoneInferred =
      [Pat ParamType] -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    [PatBase f vn t] -> SrcLoc -> PatBase f vn t
    TuplePat ([Pat ParamType] -> SrcLoc -> Pat ParamType)
    -> TermTypeM [Pat ParamType] -> TermTypeM (SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
    -> [PatBase NoInfo VName ParamType] -> TermTypeM [Pat ParamType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\PatBase NoInfo VName ParamType
    p -> [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p Inferred ParamType
    forall t. Inferred t
    NoneInferred) [PatBase NoInfo VName ParamType]
    ps TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    _ (RecordPat [(L Name, PatBase NoInfo VName ParamType)]
    p_fs SrcLoc
    _) Inferred ParamType
    _
      | Just (L Loc
    loc Name
    f, PatBase NoInfo VName ParamType
    _) <- ((L Name, PatBase NoInfo VName ParamType) -> Bool)
    -> [(L Name, PatBase NoInfo VName ParamType)]
    -> Maybe (L Name, PatBase NoInfo VName ParamType)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find (([Char]
    "_" `isPrefixOf`) ([Char] -> Bool)
    -> ((L Name, PatBase NoInfo VName ParamType) -> [Char])
    -> (L Name, PatBase NoInfo VName ParamType)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Char]
    nameToString (Name -> [Char])
    -> ((L Name, PatBase NoInfo VName ParamType) -> Name)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L Name -> Name
    forall a. L a -> a
    unLoc (L Name -> Name)
    -> ((L Name, PatBase NoInfo VName ParamType) -> L Name)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (L Name, PatBase NoInfo VName ParamType) -> L Name
    forall a b. (a, b) -> a
    fst) [(L Name, PatBase NoInfo VName ParamType)]
    p_fs =
          Loc -> Notes -> Doc () -> TermTypeM (Pat ParamType)
    forall loc a. Located loc => loc -> Notes -> Doc () -> TermTypeM a
    forall (m :: * -> *) loc a.
    (MonadTypeChecker m, Located loc) =>
    loc -> Notes -> Doc () -> m a
    typeError Loc
    loc Notes
    forall a. Monoid a => a
    mempty (Doc () -> TermTypeM (Pat ParamType))
    -> Doc () -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Underscore-prefixed fields are not allowed."
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "Did you mean"
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes ([Char] -> Doc ()
    forall ann. [Char] -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Int -> [Char] -> [Char]
    forall a. Int -> [a] -> [a]
    drop Int
    1 (Name -> [Char]
    nameToString Name
    f)) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "=_")
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "?"
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes p :: PatBase NoInfo VName ParamType
    p@(RecordPat [(L Name, PatBase NoInfo VName ParamType)]
    p_fs SrcLoc
    loc) (Ascribed ParamType
    t)
      | Scalar (Record Map Name ParamType
    t_fs) <- ParamType
    t,
        [(L Name, PatBase NoInfo VName ParamType)]
    p_fs' <- ((L Name, PatBase NoInfo VName ParamType)
     -> (L Name, PatBase NoInfo VName ParamType) -> Ordering)
    -> [(L Name, PatBase NoInfo VName ParamType)]
    -> [(L Name, PatBase NoInfo VName ParamType)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((L Name, PatBase NoInfo VName ParamType) -> L Name)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (L Name, PatBase NoInfo VName ParamType) -> L Name
    forall a b. (a, b) -> a
    fst) [(L Name, PatBase NoInfo VName ParamType)]
    p_fs,
        [(Name, ParamType)]
    t_fs' <- ((Name, ParamType) -> (Name, ParamType) -> Ordering)
    -> [(Name, ParamType)] -> [(Name, ParamType)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Name, ParamType) -> Name)
    -> (Name, ParamType) -> (Name, ParamType) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Name, ParamType) -> Name
    forall a b. (a, b) -> a
    fst) (Map Name ParamType -> [(Name, ParamType)]
    forall k a. Map k a -> [(k, a)]
    M.toList Map Name ParamType
    t_fs),
        ((Name, ParamType) -> Name) -> [(Name, ParamType)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, ParamType) -> Name
    forall a b. (a, b) -> a
    fst [(Name, ParamType)]
    t_fs' [Name] -> [Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    == ((L Name, PatBase NoInfo VName ParamType) -> Name)
    -> [(L Name, PatBase NoInfo VName ParamType)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (L Name -> Name
    forall a. L a -> a
    unLoc (L Name -> Name)
    -> ((L Name, PatBase NoInfo VName ParamType) -> L Name)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (L Name, PatBase NoInfo VName ParamType) -> L Name
    forall a b. (a, b) -> a
    fst) [(L Name, PatBase NoInfo VName ParamType)]
    p_fs' =
          [(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    [(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
    RecordPat ([(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
    -> TermTypeM [(L Name, Pat ParamType)]
    -> TermTypeM (SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((L Name, PatBase NoInfo VName ParamType)
     -> (Name, ParamType) -> TermTypeM (L Name, Pat ParamType))
    -> [(L Name, PatBase NoInfo VName ParamType)]
    -> [(Name, ParamType)]
    -> TermTypeM [(L Name, Pat ParamType)]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (L Name, PatBase NoInfo VName ParamType)
    -> (Name, ParamType) -> TermTypeM (L Name, Pat ParamType)
    forall {a} {a}.
    (L a, PatBase NoInfo VName ParamType)
    -> (a, ParamType) -> TermTypeM (L a, Pat ParamType)
    check [(L Name, PatBase NoInfo VName ParamType)]
    p_fs' [(Name, ParamType)]
    t_fs' TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
      | Bool
    otherwise = do
          Map Name StructType
    p_fs' <- (PatBase NoInfo VName ParamType -> TermTypeM StructType)
    -> Map Name (PatBase NoInfo VName ParamType)
    -> TermTypeM (Map Name StructType)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Name a -> f (Map Name b)
    traverse (TermTypeM StructType
    -> PatBase NoInfo VName ParamType -> TermTypeM StructType
    forall a b. a -> b -> a
    const (TermTypeM StructType
     -> PatBase NoInfo VName ParamType -> TermTypeM StructType)
    -> TermTypeM StructType
    -> PatBase NoInfo VName ParamType
    -> TermTypeM StructType
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Name -> TermTypeM StructType
    forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> TermTypeM (TypeBase dim als)
    forall (m :: * -> *) als a dim.
    (MonadUnify m, Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    newTypeVar SrcLoc
    loc Name
    "t") (Map Name (PatBase NoInfo VName ParamType)
     -> TermTypeM (Map Name StructType))
    -> Map Name (PatBase NoInfo VName ParamType)
    -> TermTypeM (Map Name StructType)
    forall a b. (a -> b) -> a -> b
    $ [(Name, PatBase NoInfo VName ParamType)]
    -> Map Name (PatBase NoInfo VName ParamType)
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ([(Name, PatBase NoInfo VName ParamType)]
     -> Map Name (PatBase NoInfo VName ParamType))
    -> [(Name, PatBase NoInfo VName ParamType)]
    -> Map Name (PatBase NoInfo VName ParamType)
    forall a b. (a -> b) -> a -> b
    $ ((L Name, PatBase NoInfo VName ParamType)
     -> (Name, PatBase NoInfo VName ParamType))
    -> [(L Name, PatBase NoInfo VName ParamType)]
    -> [(Name, PatBase NoInfo VName ParamType)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((L Name -> Name)
    -> (L Name, PatBase NoInfo VName ParamType)
    -> (Name, PatBase NoInfo VName ParamType)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first L Name -> Name
    forall a. L a -> a
    unLoc) [(L Name, PatBase NoInfo VName ParamType)]
    p_fs

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

          Usage -> StructType -> StructType -> TermTypeM ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify (SrcLoc -> Text -> Usage
    forall a. Located a => a -> Text -> Usage
    mkUsage SrcLoc
    loc Text
    "matching a record pattern") (ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (Map Name StructType
    -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record Map Name StructType
    p_fs')) (ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct ParamType
    t)
          [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p (Inferred ParamType -> TermTypeM (Pat ParamType))
    -> Inferred ParamType -> TermTypeM (Pat ParamType)
    forall a b. (a -> b) -> a -> b
    $ ParamType -> Inferred ParamType
    forall t. t -> Inferred t
    Ascribed (ParamType -> Inferred ParamType)
    -> ParamType -> Inferred ParamType
    forall a b. (a -> b) -> a -> b
    $ Diet -> StructType -> ParamType
    forall u. Diet -> TypeBase (ExpBase Info VName) u -> ParamType
    toParam Diet
    Observe (StructType -> ParamType) -> StructType -> ParamType
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase (ExpBase Info VName) NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (Map Name StructType
    -> ScalarTypeBase (ExpBase Info VName) NoUniqueness
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record Map Name StructType
    p_fs')
      where
        check :: (L a, PatBase NoInfo VName ParamType)
    -> (a, ParamType) -> TermTypeM (L a, Pat ParamType)
    check (L Loc
    f_loc a
    f, PatBase NoInfo VName ParamType
    p_f) (a
    _, ParamType
    t_f) = (Loc -> a -> L a
    forall a. Loc -> a -> L a
    L Loc
    f_loc a
    f,) (Pat ParamType -> (L a, Pat ParamType))
    -> TermTypeM (Pat ParamType) -> TermTypeM (L a, Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p_f (ParamType -> Inferred ParamType
    forall t. t -> Inferred t
    Ascribed ParamType
    t_f)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes (RecordPat [(L Name, PatBase NoInfo VName ParamType)]
    fs SrcLoc
    loc) Inferred ParamType
    NoneInferred =
      [(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType
    forall (f :: * -> *) vn t.
    [(L Name, PatBase f vn t)] -> SrcLoc -> PatBase f vn t
    RecordPat ([(L Name, Pat ParamType)] -> SrcLoc -> Pat ParamType)
    -> (Map (L Name) (Pat ParamType) -> [(L Name, Pat ParamType)])
    -> Map (L Name) (Pat ParamType)
    -> SrcLoc
    -> Pat ParamType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map (L Name) (Pat ParamType) -> [(L Name, Pat ParamType)]
    forall k a. Map k a -> [(k, a)]
    M.toList
        (Map (L Name) (Pat ParamType) -> SrcLoc -> Pat ParamType)
    -> TermTypeM (Map (L Name) (Pat ParamType))
    -> TermTypeM (SrcLoc -> Pat ParamType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (PatBase NoInfo VName ParamType -> TermTypeM (Pat ParamType))
    -> Map (L Name) (PatBase NoInfo VName ParamType)
    -> TermTypeM (Map (L Name) (Pat ParamType))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map (L Name) a -> f (Map (L Name) b)
    traverse (\PatBase NoInfo VName ParamType
    p -> [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName ParamType
    -> Inferred ParamType
    -> TermTypeM (Pat ParamType)
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes PatBase NoInfo VName ParamType
    p Inferred ParamType
    forall t. Inferred t
    NoneInferred) ([(L Name, PatBase NoInfo VName ParamType)]
    -> Map (L Name) (PatBase NoInfo VName ParamType)
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(L Name, PatBase NoInfo VName ParamType)]
    fs)
        TermTypeM (SrcLoc -> Pat ParamType)
    -> TermTypeM SrcLoc -> TermTypeM (Pat ParamType)
    forall a b. TermTypeM (a -> b) -> TermTypeM a -> TermTypeM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SrcLoc -> TermTypeM SrcLoc
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SrcLoc
    loc
    checkPat' [(SizeBinder VName, QualName VName)]
    sizes (PatAscription PatBase NoInfo VName ParamType
    p TypeExp (ExpBase NoInfo VName) VName
    t SrcLoc
    loc) Inferred ParamType
    maybe_outer_t = do
      (TypeExp (ExpBase Info VName) VName
    t', ResType
    st, [VName]
    _) <- TypeExp (ExpBase NoInfo VName) VName
    -> TermTypeM (TypeExp (ExpBase Info VName) VName, ResType, [VName])
    checkTypeExpNonrigid TypeExp (ExpBase NoInfo VName) VName
    t

      case Inferred ParamType
    maybe_outer_t of
        Ascribed ParamType
    outer_t -> do
          let st_forunify :: StructType
    st_forunify = [(SizeBinder VName, QualName VName)] -> StructType -> StructType
    nonrigidFor [(SizeBinder VName, QualName VName)]
    sizes (StructType -> StructType) -> StructType -> StructType
    forall a b. (a -> b) -> a -> b
    $ ResType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct ResType
    st
          Usage -> StructType -> StructType -> TermTypeM ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify (SrcLoc -> Text -> Usage
    forall a. Located a => a -> Text -> Usage
    mkUsage SrcLoc
    loc Text
    "explicit type ascription") StructType
    st_forunify (ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct ParamType
    outer_t)

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

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

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

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

    -- | Check and bind a @let@-pattern.
    bindingPat ::
      [SizeBinder VName] ->
      PatBase NoInfo VName (TypeBase Size u) ->
      StructType ->
      (Pat ParamType -> TermTypeM a) ->
      TermTypeM a
    bindingPat :: forall u a.
    [SizeBinder VName]
    -> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    -> StructType
    -> (Pat ParamType -> TermTypeM a)
    -> TermTypeM a
    bindingPat [SizeBinder VName]
    sizes PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    p StructType
    t Pat ParamType -> TermTypeM a
    m = do
      [(SizeBinder VName, QualName VName)]
    substs <- (SizeBinder VName -> TermTypeM (SizeBinder VName, QualName VName))
    -> [SizeBinder VName]
    -> TermTypeM [(SizeBinder VName, QualName VName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SizeBinder VName -> TermTypeM (SizeBinder VName, QualName VName)
    mkSizeSubst [SizeBinder VName]
    sizes
      [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    -> Inferred StructType
    -> (Pat ParamType -> TermTypeM a)
    -> TermTypeM a
    forall u a.
    [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    -> Inferred StructType
    -> (Pat ParamType -> TermTypeM a)
    -> TermTypeM a
    checkPat [(SizeBinder VName, QualName VName)]
    substs PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    p (StructType -> Inferred StructType
    forall t. t -> Inferred t
    Ascribed StructType
    t) ((Pat ParamType -> TermTypeM a) -> TermTypeM a)
    -> (Pat ParamType -> TermTypeM a) -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ \Pat ParamType
    p' -> [Ident StructType] -> TermTypeM a -> TermTypeM a
    forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
    binding (PatBase Info VName StructType -> [Ident StructType]
    forall (f :: * -> *) vn t. PatBase f vn t -> [IdentBase f vn t]
    patIdents ((ParamType -> StructType)
    -> Pat ParamType -> PatBase Info VName StructType
    forall a b.
    (a -> b) -> PatBase Info VName a -> PatBase Info VName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct Pat ParamType
    p')) (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $
        case (SizeBinder VName -> Bool)
    -> [SizeBinder VName] -> [SizeBinder VName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.notMember` FV -> Set VName
    fvVars (Pat ParamType -> FV
    forall u. Pat (TypeBase (ExpBase Info VName) u) -> FV
    freeInPat Pat ParamType
    p')) (VName -> Bool)
    -> (SizeBinder VName -> VName) -> SizeBinder VName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeBinder VName -> VName
    forall vn. SizeBinder vn -> vn
    sizeName) [SizeBinder VName]
    sizes of
          [] -> Pat ParamType -> TermTypeM a
    m Pat ParamType
    p'
          SizeBinder VName
    size : [SizeBinder VName]
    _ -> SizeBinder VName -> TermTypeM a
    forall (m :: * -> *) a.
    MonadTypeChecker m =>
    SizeBinder VName -> m a
    unusedSize SizeBinder VName
    size
      where
        mkSizeSubst :: SizeBinder VName -> TermTypeM (SizeBinder VName, QualName VName)
    mkSizeSubst SizeBinder VName
    v = do
          VName
    v' <- Name -> TermTypeM VName
    forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
    newID (Name -> TermTypeM VName) -> Name -> TermTypeM VName
    forall a b. (a -> b) -> a -> b
    $ VName -> Name
    baseName (VName -> Name) -> VName -> Name
    forall a b. (a -> b) -> a -> b
    $ SizeBinder VName -> VName
    forall vn. SizeBinder vn -> vn
    sizeName SizeBinder VName
    v
          VName -> Constraint -> TermTypeM ()
    constrain VName
    v' (Constraint -> TermTypeM ())
    -> (Usage -> Constraint) -> Usage -> TermTypeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe (ExpBase Info VName) -> Usage -> Constraint
    Size Maybe (ExpBase Info VName)
    forall a. Maybe a
    Nothing (Usage -> TermTypeM ()) -> Usage -> TermTypeM ()
    forall a b. (a -> b) -> a -> b
    $
            SizeBinder VName -> Text -> Usage
    forall a. Located a => a -> Text -> Usage
    mkUsage SizeBinder VName
    v Text
    "ambiguous size of bound expression"
          (SizeBinder VName, QualName VName)
    -> TermTypeM (SizeBinder VName, QualName VName)
    forall a. a -> TermTypeM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SizeBinder VName
    v, VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    v')

    -- | Check and bind type and value parameters.
    bindingParams ::
      [TypeParam] ->
      [PatBase NoInfo VName ParamType] ->
      ([Pat ParamType] -> TermTypeM a) ->
      TermTypeM a
    bindingParams :: forall a.
    [TypeParam]
    -> [PatBase NoInfo VName ParamType]
    -> ([Pat ParamType] -> TermTypeM a)
    -> TermTypeM a
    bindingParams [TypeParam]
    tps [PatBase NoInfo VName ParamType]
    orig_ps [Pat ParamType] -> TermTypeM a
    m = [TypeParam] -> TermTypeM a -> TermTypeM a
    forall a. [TypeParam] -> TermTypeM a -> TermTypeM a
    bindingTypeParams [TypeParam]
    tps (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ do
      let descend :: [Pat ParamType]
    -> [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
    -> TermTypeM a
    descend [Pat ParamType]
    ps' (PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    p : [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
    ps) =
            [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    -> Inferred StructType
    -> (Pat ParamType -> TermTypeM a)
    -> TermTypeM a
    forall u a.
    [(SizeBinder VName, QualName VName)]
    -> PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    -> Inferred StructType
    -> (Pat ParamType -> TermTypeM a)
    -> TermTypeM a
    checkPat [] PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)
    p Inferred StructType
    forall t. Inferred t
    NoneInferred ((Pat ParamType -> TermTypeM a) -> TermTypeM a)
    -> (Pat ParamType -> TermTypeM a) -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ \Pat ParamType
    p' ->
              [Ident StructType] -> TermTypeM a -> TermTypeM a
    forall a. [Ident StructType] -> TermTypeM a -> TermTypeM a
    binding (PatBase Info VName StructType -> [Ident StructType]
    forall (f :: * -> *) vn t. PatBase f vn t -> [IdentBase f vn t]
    patIdents (PatBase Info VName StructType -> [Ident StructType])
    -> PatBase Info VName StructType -> [Ident StructType]
    forall a b. (a -> b) -> a -> b
    $ (ParamType -> StructType)
    -> Pat ParamType -> PatBase Info VName StructType
    forall a b.
    (a -> b) -> PatBase Info VName a -> PatBase Info VName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ParamType -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct Pat ParamType
    p') (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ TermTypeM a -> TermTypeM a
    forall a. TermTypeM a -> TermTypeM a
    incLevel (TermTypeM a -> TermTypeM a) -> TermTypeM a -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ [Pat ParamType]
    -> [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
    -> TermTypeM a
    descend (Pat ParamType
    p' Pat ParamType -> [Pat ParamType] -> [Pat ParamType]
    forall a. a -> [a] -> [a]
    : [Pat ParamType]
    ps') [PatBase NoInfo VName (TypeBase (ExpBase Info VName) u)]
    ps
          descend [Pat ParamType]
    ps' [] = [Pat ParamType] -> TermTypeM a
    m ([Pat ParamType] -> TermTypeM a) -> [Pat ParamType] -> TermTypeM a
    forall a b. (a -> b) -> a -> b
    $ [Pat ParamType] -> [Pat ParamType]
    forall a. [a] -> [a]
    reverse [Pat ParamType]
    ps'

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