    -- |
    -- Module      :  Cryptol.TypeCheck.Kind
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE RecursiveDo #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Kind
      ( checkType
      , checkSchema
      , checkNewtype
      , checkPrimType
      , checkTySyn
      , checkPropSyn
      , checkParameterType
      , checkParameterConstraints
      ) where

    import qualified Cryptol.Parser.AST as P
    import           Cryptol.Parser.AST (Named(..))
    import           Cryptol.Parser.Position
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.Error
    import           Cryptol.TypeCheck.Monad hiding (withTParams)
    import           Cryptol.TypeCheck.SimpType(tRebuild)
    import           Cryptol.TypeCheck.SimpleSolver(simplify)
    import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)
    import           Cryptol.TypeCheck.Subst(listSubst,apSubst)
    import           Cryptol.Utils.Panic (panic)

    import qualified Data.Map as Map
    import           Data.List(sortBy,groupBy)
    import           Data.Maybe(fromMaybe)
    import           Data.Function(on)
    import           Control.Monad(unless,forM,when)

    -- | Check a type signature.  Returns validated schema, and any implicit
    -- constraints that we inferred.
    checkSchema :: AllowWildCards -> P.Schema Name -> InferM (Schema, [Goal])
    checkSchema :: AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
    checkSchema withWild :: AllowWildCards
    withWild (P.Forall xs :: [TParam Name]
    xs ps :: [Prop Name]
    ps t :: Type Name
    t mb :: Maybe Range
    mb) =
      do ((xs1 :: [TParam]
    xs1,(ps1 :: [Type]
    ps1,t1 :: Type
    t1)), gs :: [Goal]
    gs) <-
            InferM ([TParam], ([Type], Type))
    -> InferM (([TParam], ([Type], Type)), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals (InferM ([TParam], ([Type], Type))
     -> InferM (([TParam], ([Type], Type)), [Goal]))
    -> InferM ([TParam], ([Type], Type))
    -> InferM (([TParam], ([Type], Type)), [Goal])
    forall a b. (a -> b) -> a -> b
    $
            InferM ([TParam], ([Type], Type))
    -> InferM ([TParam], ([Type], Type))
    forall a. InferM a -> InferM a
    rng (InferM ([TParam], ([Type], Type))
     -> InferM ([TParam], ([Type], Type)))
    -> InferM ([TParam], ([Type], Type))
    -> InferM ([TParam], ([Type], Type))
    forall a b. (a -> b) -> a -> b
    $ AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM ([Type], Type)
    -> InferM ([TParam], ([Type], Type))
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    withWild Name -> TPFlavor
    schemaParam [TParam Name]
    xs (KindM ([Type], Type) -> InferM ([TParam], ([Type], Type)))
    -> KindM ([Type], Type) -> InferM ([TParam], ([Type], Type))
    forall a b. (a -> b) -> a -> b
    $
            do [Type]
    ps1 <- (Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Prop Name -> KindM Type
    checkProp [Prop Name]
    ps
               Type
    t1  <- Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)
               ([Type], Type) -> KindM ([Type], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type]
    ps1,Type
    t1)
         -- XXX: We probably shouldn't do this, as we are changing what the
         -- user is doing.  We do it so that things are in a propal normal form,
         -- but we should probably figure out another time to do this.
         let newPs :: [Type]
    newPs = (Type -> [Type]) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Type -> [Type]
    pSplitAnd ([Type] -> [Type]) -> [Type] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ctxt -> Type -> Type
    simplify Ctxt
    forall k a. Map k a
    Map.empty)
                                         ([Type] -> [Type]) -> [Type] -> [Type]
    forall a b. (a -> b) -> a -> b
    $ (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    tRebuild [Type]
    ps1
         (Schema, [Goal]) -> InferM (Schema, [Goal])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( [TParam] -> [Type] -> Type -> Schema
    Forall [TParam]
    xs1 [Type]
    newPs (Type -> Type
    tRebuild Type
    t1)
                , [ Goal
    g { goal :: Type
    goal = Type -> Type
    tRebuild (Goal -> Type
    goal Goal
    g) } | Goal
    g <- [Goal]
    gs ]
                )

      where
      rng :: InferM a -> InferM a
    rng = case Maybe Range
    mb of
              Nothing -> InferM a -> InferM a
    forall a. a -> a
    id
              Just r :: Range
    r  -> Range -> InferM a -> InferM a
    forall a. Range -> InferM a -> InferM a
    inRange Range
    r

    -- | Check a module parameter declarations.  Nothing much to check,
    -- we just translate from one syntax to another.
    checkParameterType :: P.ParameterType Name -> Maybe String -> InferM ModTParam
    checkParameterType :: ParameterType Name -> Maybe String -> InferM ModTParam
    checkParameterType a :: ParameterType Name
    a mbDoc :: Maybe String
    mbDoc =
      do let k :: Kind
    k = Kind -> Kind
    cvtK (ParameterType Name -> Kind
    forall name. ParameterType name -> Kind
    P.ptKind ParameterType Name
    a)
             n :: Name
    n = Located Name -> Name
    forall a. Located a -> a
    thing (ParameterType Name -> Located Name
    forall name. ParameterType name -> Located name
    P.ptName ParameterType Name
    a)
         ModTParam -> InferM ModTParam
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WModTParam :: Name -> Kind -> Int -> Maybe String -> ModTParam
    ModTParam { mtpKind :: Kind
    mtpKind = Kind
    k, mtpName :: Name
    mtpName = Name
    n, mtpDoc :: Maybe String
    mtpDoc = Maybe String
    mbDoc
                          , mtpNumber :: Int
    mtpNumber = ParameterType Name -> Int
    forall name. ParameterType name -> Int
    P.ptNumber ParameterType Name
    a }

    -- | Check a type-synonym declaration.
    checkTySyn :: P.TySyn Name -> Maybe String -> InferM TySyn
    checkTySyn :: TySyn Name -> Maybe String -> InferM TySyn
    checkTySyn (P.TySyn x :: Located Name
    x _ as :: [TParam Name]
    as t :: Type Name
    t) mbD :: Maybe String
    mbD =
      do ((as1 :: [TParam]
    as1,t1 :: Type
    t1),gs :: [Goal]
    gs) <- InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals
                        (InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal]))
    -> InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal])
    forall a b. (a -> b) -> a -> b
    $ Range -> InferM ([TParam], Type) -> InferM ([TParam], Type)
    forall a. Range -> InferM a -> InferM a
    inRange (Located Name -> Range
    forall a. Located a -> Range
    srcRange Located Name
    x)
                        (InferM ([TParam], Type) -> InferM ([TParam], Type))
    -> InferM ([TParam], Type) -> InferM ([TParam], Type)
    forall a b. (a -> b) -> a -> b
    $ do ([TParam], Type)
    r <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM Type
    -> InferM ([TParam], Type)
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    tySynParam [TParam Name]
    as
                                                          (Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t Maybe Kind
    forall a. Maybe a
    Nothing)
                             InferM ()
    simplifyAllConstraints
                             ([TParam], Type) -> InferM ([TParam], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam], Type)
    r
         TySyn -> InferM TySyn
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WTySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe String -> TySyn
    TySyn { tsName :: Name
    tsName   = Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x
                      , tsParams :: [TParam]
    tsParams = [TParam]
    as1
                      , tsConstraints :: [Type]
    tsConstraints = (Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type -> Type
    tRebuild (Type -> Type) -> (Goal -> Type) -> Goal -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Type
    goal) [Goal]
    gs
                      , tsDef :: Type
    tsDef = Type -> Type
    tRebuild Type
    t1
                      , tsDoc :: Maybe String
    tsDoc = Maybe String
    mbD
                      }

    -- | Check a constraint-synonym declaration.
    checkPropSyn :: P.PropSyn Name -> Maybe String -> InferM TySyn
    checkPropSyn :: PropSyn Name -> Maybe String -> InferM TySyn
    checkPropSyn (P.PropSyn x :: Located Name
    x _ as :: [TParam Name]
    as ps :: [Prop Name]
    ps) mbD :: Maybe String
    mbD =
      do ((as1 :: [TParam]
    as1,t1 :: [Type]
    t1),gs :: [Goal]
    gs) <- InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals
                        (InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal]))
    -> InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal])
    forall a b. (a -> b) -> a -> b
    $ Range -> InferM ([TParam], [Type]) -> InferM ([TParam], [Type])
    forall a. Range -> InferM a -> InferM a
    inRange (Located Name -> Range
    forall a. Located a -> Range
    srcRange Located Name
    x)
                        (InferM ([TParam], [Type]) -> InferM ([TParam], [Type]))
    -> InferM ([TParam], [Type]) -> InferM ([TParam], [Type])
    forall a b. (a -> b) -> a -> b
    $ do ([TParam], [Type])
    r <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [Type]
    -> InferM ([TParam], [Type])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    propSynParam [TParam Name]
    as
                                                          ((Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Prop Name -> KindM Type
    checkProp [Prop Name]
    ps)
                             InferM ()
    simplifyAllConstraints
                             ([TParam], [Type]) -> InferM ([TParam], [Type])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam], [Type])
    r
         TySyn -> InferM TySyn
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WTySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe String -> TySyn
    TySyn { tsName :: Name
    tsName   = Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x
                      , tsParams :: [TParam]
    tsParams = [TParam]
    as1
                      , tsConstraints :: [Type]
    tsConstraints = (Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type -> Type
    tRebuild (Type -> Type) -> (Goal -> Type) -> Goal -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Type
    goal) [Goal]
    gs
                      , tsDef :: Type
    tsDef = Type -> Type
    tRebuild ([Type] -> Type
    pAnd [Type]
    t1)
                      , tsDoc :: Maybe String
    tsDoc = Maybe String
    mbD
                      }

    -- | Check a newtype declaration.
    -- XXX: Do something with constraints.
    checkNewtype :: P.Newtype Name -> Maybe String -> InferM Newtype
    checkNewtype :: Newtype Name -> Maybe String -> InferM Newtype
    checkNewtype (P.Newtype x :: Located Name
    x as :: [TParam Name]
    as fs :: [Named (Type Name)]
    fs) mbD :: Maybe String
    mbD =
      do ((as1 :: [TParam]
    as1,fs1 :: [(Ident, Type)]
    fs1),gs :: [Goal]
    gs) <- InferM ([TParam], [(Ident, Type)])
    -> InferM (([TParam], [(Ident, Type)]), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals (InferM ([TParam], [(Ident, Type)])
     -> InferM (([TParam], [(Ident, Type)]), [Goal]))
    -> InferM ([TParam], [(Ident, Type)])
    -> InferM (([TParam], [(Ident, Type)]), [Goal])
    forall a b. (a -> b) -> a -> b
    $
           Range
    -> InferM ([TParam], [(Ident, Type)])
    -> InferM ([TParam], [(Ident, Type)])
    forall a. Range -> InferM a -> InferM a
    inRange (Located Name -> Range
    forall a. Located a -> Range
    srcRange Located Name
    x) (InferM ([TParam], [(Ident, Type)])
     -> InferM ([TParam], [(Ident, Type)]))
    -> InferM ([TParam], [(Ident, Type)])
    -> InferM ([TParam], [(Ident, Type)])
    forall a b. (a -> b) -> a -> b
    $
           do ([TParam], [(Ident, Type)])
    r <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [(Ident, Type)]
    -> InferM ([TParam], [(Ident, Type)])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    newtypeParam [TParam Name]
    as (KindM [(Ident, Type)] -> InferM ([TParam], [(Ident, Type)]))
    -> KindM [(Ident, Type)] -> InferM ([TParam], [(Ident, Type)])
    forall a b. (a -> b) -> a -> b
    $
                   [Named (Type Name)]
    -> (Named (Type Name) -> KindM (Ident, Type))
    -> KindM [(Ident, Type)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Named (Type Name)]
    fs ((Named (Type Name) -> KindM (Ident, Type))
     -> KindM [(Ident, Type)])
    -> (Named (Type Name) -> KindM (Ident, Type))
    -> KindM [(Ident, Type)]
    forall a b. (a -> b) -> a -> b
    $ \field :: Named (Type Name)
    field ->
                     let n :: Located Ident
    n = Named (Type Name) -> Located Ident
    forall a. Named a -> Located Ident
    name Named (Type Name)
    field
                     in Range -> KindM (Ident, Type) -> KindM (Ident, Type)
    forall a. Range -> KindM a -> KindM a
    kInRange (Located Ident -> Range
    forall a. Located a -> Range
    srcRange Located Ident
    n) (KindM (Ident, Type) -> KindM (Ident, Type))
    -> KindM (Ident, Type) -> KindM (Ident, Type)
    forall a b. (a -> b) -> a -> b
    $
                        do Type
    t1 <- Type Name -> Maybe Kind -> KindM Type
    doCheckType (Named (Type Name) -> Type Name
    forall a. Named a -> a
    value Named (Type Name)
    field) (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)
                           (Ident, Type) -> KindM (Ident, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Located Ident -> Ident
    forall a. Located a -> a
    thing Located Ident
    n, Type
    t1)
              InferM ()
    simplifyAllConstraints
              ([TParam], [(Ident, Type)]) -> InferM ([TParam], [(Ident, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam], [(Ident, Type)])
    r

         Newtype -> InferM Newtype
    forall (m :: * -> *) a. Monad m => a -> m a
    return Newtype :: Name
    -> [TParam] -> [Type] -> [(Ident, Type)] -> Maybe String -> Newtype
    Newtype { ntName :: Name
    ntName   = Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x
                        , ntParams :: [TParam]
    ntParams = [TParam]
    as1
                        , ntConstraints :: [Type]
    ntConstraints = (Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Type
    goal [Goal]
    gs
                        , ntFields :: [(Ident, Type)]
    ntFields = [(Ident, Type)]
    fs1
                        , ntDoc :: Maybe String
    ntDoc = Maybe String
    mbD
                        }

    checkPrimType :: P.PrimType Name -> Maybe String -> InferM AbstractType
    checkPrimType :: PrimType Name -> Maybe String -> InferM AbstractType
    checkPrimType p :: PrimType Name
    p mbD :: Maybe String
    mbD =
      do let (as :: [TParam Name]
    as,cs :: [Prop Name]
    cs) = PrimType Name -> ([TParam Name], [Prop Name])
    forall name. PrimType name -> ([TParam name], [Prop name])
    P.primTCts PrimType Name
    p
         (as' :: [TParam]
    as',cs' :: [Type]
    cs') <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [Type]
    -> InferM ([TParam], [Type])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards (Maybe Name -> TPFlavor
    TPOther (Maybe Name -> TPFlavor)
    -> (Name -> Maybe Name) -> Name -> TPFlavor
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Maybe Name
    forall a. a -> Maybe a
    Just) [TParam Name]
    as (KindM [Type] -> InferM ([TParam], [Type]))
    -> KindM [Type] -> InferM ([TParam], [Type])
    forall a b. (a -> b) -> a -> b
    $
                        (Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Prop Name -> KindM Type
    checkProp [Prop Name]
    cs
         AbstractType -> InferM AbstractType
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure AbstractType :: Name
    -> Kind
    -> ([TParam], [Type])
    -> Maybe Fixity
    -> Maybe String
    -> AbstractType
    AbstractType { atName :: Name
    atName = Located Name -> Name
    forall a. Located a -> a
    thing (PrimType Name -> Located Name
    forall name. PrimType name -> Located name
    P.primTName PrimType Name
    p)
                           , atKind :: Kind
    atKind = Kind -> Kind
    cvtK (Located Kind -> Kind
    forall a. Located a -> a
    thing (PrimType Name -> Located Kind
    forall name. PrimType name -> Located Kind
    P.primTKind PrimType Name
    p))
                           , atFixitiy :: Maybe Fixity
    atFixitiy = PrimType Name -> Maybe Fixity
    forall name. PrimType name -> Maybe Fixity
    P.primTFixity PrimType Name
    p
                           , atCtrs :: ([TParam], [Type])
    atCtrs = ([TParam]
    as',[Type]
    cs')
                           , atDoc :: Maybe String
    atDoc = Maybe String
    mbD
                           }

    checkType :: P.Type Name -> Maybe Kind -> InferM Type
    checkType :: Type Name -> Maybe Kind -> InferM Type
    checkType t :: Type Name
    t k :: Maybe Kind
    k =
      do (_, t1 :: Type
    t1) <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM Type
    -> InferM ([TParam], Type)
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    AllowWildCards Name -> TPFlavor
    schemaParam [] (KindM Type -> InferM ([TParam], Type))
    -> KindM Type -> InferM ([TParam], Type)
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t Maybe Kind
    k
         Type -> InferM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Type
    tRebuild Type
    t1)

    checkParameterConstraints :: [Located (P.Prop Name)] -> InferM [Located Prop]
    checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Type]
    checkParameterConstraints ps :: [Located (Prop Name)]
    ps =
      do (_, cs :: [Located Type]
    cs) <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [Located Type]
    -> InferM ([TParam], [Located Type])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    schemaParam [] ((Located (Prop Name) -> KindM (Located Type))
    -> [Located (Prop Name)] -> KindM [Located Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Located (Prop Name) -> KindM (Located Type)
    checkL [Located (Prop Name)]
    ps)
         [Located Type] -> InferM [Located Type]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Located Type]
    cs
      where
      checkL :: Located (Prop Name) -> KindM (Located Type)
    checkL x :: Located (Prop Name)
    x = do Type
    p <- Prop Name -> KindM Type
    checkProp (Located (Prop Name) -> Prop Name
    forall a. Located a -> a
    thing Located (Prop Name)
    x)
                    Located Type -> KindM (Located Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Located (Prop Name)
    x { thing :: Type
    thing = Type -> Type
    tRebuild Type
    p }

    {- | Check something with type parameters.

    When we check things with type parameters (i.e., type schemas, and type
    synonym declarations) we do kind inference based only on the immediately
    visible body.  Type parameters that are not mentioned in the body are
    defaulted to kind 'KNum'.  If this is not the desired behavior, programmers
    may add explicit kind annotations on the type parameters.

    Here is an example of how this may show up:

    > f : {n}. [8] -> [8]
    > f x =  x + `n

    Note that @n@ does not appear in the body of the schema, so we will
    default it to 'KNum', which is the correct thing in this case.
    To use such a function, we'd have to provide an explicit type application:

    > f `{n = 3}

    There are two reasons for this choice:

      1. It makes it possible to figure if something is correct without
         having to look through arbitrary amounts of code.

      2. It is a bit easier to implement, and it covers the large majority
         of use cases, with a very small inconvenience (an explicit kind
         annotation) in the rest.
    -}

    withTParams :: AllowWildCards    {- ^ Do we allow wild cards -} ->
                  (Name -> TPFlavor) {- ^ What sort of params are these? -} ->
                  [P.TParam Name]    {- ^ The params -} ->
                  KindM a            {- ^ do this using the params -} ->
                  InferM ([TParam], a)
    withTParams :: AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams allowWildCards :: AllowWildCards
    allowWildCards flav :: Name -> TPFlavor
    flav xs :: [TParam Name]
    xs m :: KindM a
    m
      | Bool -> Bool
    not ([[TParam Name]] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [[TParam Name]]
    duplicates) = String -> [String] -> InferM ([TParam], a)
    forall a. HasCallStack => String -> [String] -> a
    panic "withTParams" ([String] -> InferM ([TParam], a))
    -> [String] -> InferM ([TParam], a)
    forall a b. (a -> b) -> a -> b
    $ "Repeated parameters"
                                                    String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : ([TParam Name] -> String) -> [[TParam Name]] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map [TParam Name] -> String
    forall a. Show a => a -> String
    show [[TParam Name]]
    duplicates
      | Bool
    otherwise =
      do (as :: [TParam]
    as,a :: a
    a,ctrs :: [(ConstraintSource, [Type])]
    ctrs) <-
            mdo (a :: a
    a, vars :: Map Name Kind
    vars,ctrs :: [(ConstraintSource, [Type])]
    ctrs) <- AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Type])])
    forall a.
    AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Type])])
    runKindM AllowWildCards
    allowWildCards ([TParam Name] -> [TParam] -> [(Name, Maybe Kind, TParam)]
    forall n c. [TParam n] -> [c] -> [(n, Maybe Kind, c)]
    zip' [TParam Name]
    xs [TParam]
    as) KindM a
    m
                [TParam]
    as <- (TParam Name -> InferM TParam) -> [TParam Name] -> InferM [TParam]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Map Name Kind -> TParam Name -> InferM TParam
    newTP Map Name Kind
    vars) [TParam Name]
    xs
                ([TParam], a, [(ConstraintSource, [Type])])
    -> InferM ([TParam], a, [(ConstraintSource, [Type])])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam]
    as,a
    a,[(ConstraintSource, [Type])]
    ctrs)
         ((ConstraintSource, [Type]) -> InferM ())
    -> [(ConstraintSource, [Type])] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((ConstraintSource -> [Type] -> InferM ())
    -> (ConstraintSource, [Type]) -> InferM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ConstraintSource -> [Type] -> InferM ()
    newGoals) [(ConstraintSource, [Type])]
    ctrs
         ([TParam], a) -> InferM ([TParam], a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam]
    as,a
    a)

      where
      getKind :: Map Name Kind -> TParam Name -> InferM Kind
    getKind vs :: Map Name Kind
    vs tp :: TParam Name
    tp =
        case Name -> Map Name Kind -> Maybe Kind
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (TParam Name -> Name
    forall n. TParam n -> n
    P.tpName TParam Name
    tp) Map Name Kind
    vs of
          Just k :: Kind
    k  -> Kind -> InferM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
          Nothing -> do Warning -> InferM ()
    recordWarning (TParam Name -> Kind -> Warning
    DefaultingKind TParam Name
    tp Kind
    P.KNum)
                        Kind -> InferM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KNum

      newTP :: Map Name Kind -> TParam Name -> InferM TParam
    newTP vs :: Map Name Kind
    vs tp :: TParam Name
    tp = do Kind
    k <- Map Name Kind -> TParam Name -> InferM Kind
    getKind Map Name Kind
    vs TParam Name
    tp
                       let nm :: Name
    nm = TParam Name -> Name
    forall n. TParam n -> n
    P.tpName TParam Name
    tp
                       TParam Name -> TPFlavor -> Kind -> InferM TParam
    newTParam TParam Name
    tp (Name -> TPFlavor
    flav Name
    nm) Kind
    k

      {- Note that we only zip based on the first argument.
      This is needed to make the monadic recursion work correctly,
      because the data dependency is only on the part that is known. -}
      zip' :: [TParam n] -> [c] -> [(n, Maybe Kind, c)]
    zip' [] _           = []
      zip' (a :: TParam n
    a:as :: [TParam n]
    as) ~(t :: c
    t:ts :: [c]
    ts) = (TParam n -> n
    forall n. TParam n -> n
    P.tpName TParam n
    a, (Kind -> Kind) -> Maybe Kind -> Maybe Kind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Kind -> Kind
    cvtK (TParam n -> Maybe Kind
    forall n. TParam n -> Maybe Kind
    P.tpKind TParam n
    a), c
    t) (n, Maybe Kind, c) -> [(n, Maybe Kind, c)] -> [(n, Maybe Kind, c)]
    forall a. a -> [a] -> [a]
    : [TParam n] -> [c] -> [(n, Maybe Kind, c)]
    zip' [TParam n]
    as [c]
    ts

      duplicates :: [[TParam Name]]
    duplicates = [ [TParam Name]
    ds | ds :: [TParam Name]
    ds@(_ : _ : _) <- (TParam Name -> TParam Name -> Bool)
    -> [TParam Name] -> [[TParam Name]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Name -> Name -> Bool)
    -> (TParam Name -> Name) -> TParam Name -> TParam Name -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` TParam Name -> Name
    forall n. TParam n -> n
    P.tpName)
                                          ([TParam Name] -> [[TParam Name]])
    -> [TParam Name] -> [[TParam Name]]
    forall a b. (a -> b) -> a -> b
    $ (TParam Name -> TParam Name -> Ordering)
    -> [TParam Name] -> [TParam Name]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Name -> Name -> Ordering)
    -> (TParam Name -> Name) -> TParam Name -> TParam Name -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` TParam Name -> Name
    forall n. TParam n -> n
    P.tpName) [TParam Name]
    xs ]

    cvtK :: P.Kind -> Kind
    cvtK :: Kind -> Kind
    cvtK P.KNum  = Kind
    KNum
    cvtK P.KType = Kind
    KType
    cvtK P.KProp = Kind
    KProp
    cvtK (P.KFun k1 :: Kind
    k1 k2 :: Kind
    k2) = Kind -> Kind
    cvtK Kind
    k1 Kind -> Kind -> Kind
    :-> Kind -> Kind
    cvtK Kind
    k2

    -- | Check an application of a type constant.
    tcon :: TCon            -- ^ Type constant being applied
         -> [P.Type Name]   -- ^ Type parameters
         -> Maybe Kind      -- ^ Expected kind
         -> KindM Type      -- ^ Resulting type
    tcon :: TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon tc :: TCon
    tc ts0 :: [Type Name]
    ts0 k :: Maybe Kind
    k =
      do (ts1 :: [Type]
    ts1,k1 :: Kind
    k1) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts0 (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc)
         Type -> Maybe Kind -> Kind -> KindM Type
    checkKind (TCon -> [Type] -> Type
    TCon TCon
    tc [Type]
    ts1) Maybe Kind
    k Kind
    k1

    -- | Check a type application of a non built-in type or type variable.
    checkTUser ::
      Name          {- ^ The name that is being applied to some arguments. -} ->
      [P.Type Name] {- ^ Parameters to the type -} ->
      Maybe Kind    {- ^ Expected kind -} ->
      KindM Type    {- ^ Resulting type -}
    checkTUser :: Name -> [Type Name] -> Maybe Kind -> KindM Type
    checkTUser x :: Name
    x ts :: [Type Name]
    ts k :: Maybe Kind
    k =
      (Name -> KindM (Maybe LkpTyVar))
    -> (LkpTyVar -> KindM Type) -> KindM Type -> KindM Type
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase Name -> KindM (Maybe LkpTyVar)
    kLookupTyVar      LkpTyVar -> KindM Type
    checkBoundVarUse (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe TySyn))
    -> (TySyn -> KindM Type) -> KindM Type -> KindM Type
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase Name -> KindM (Maybe TySyn)
    kLookupTSyn       TySyn -> KindM Type
    checkTySynUse (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe Newtype))
    -> (Newtype -> KindM Type) -> KindM Type -> KindM Type
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase Name -> KindM (Maybe Newtype)
    kLookupNewtype    Newtype -> KindM Type
    checkNewTypeUse (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe ModTParam))
    -> (ModTParam -> KindM Type) -> KindM Type -> KindM Type
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase Name -> KindM (Maybe ModTParam)
    kLookupParamType  ModTParam -> KindM Type
    checkModuleParamUse (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe AbstractType))
    -> (AbstractType -> KindM Type) -> KindM Type -> KindM Type
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase Name -> KindM (Maybe AbstractType)
    kLookupAbstractType AbstractType -> KindM Type
    checkAbstractTypeUse (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $
      KindM Type
    checkScopedVarUse -- none of the above, must be a scoped type variable,
                        -- if the renamer did its job correctly.
      where
      checkTySynUse :: TySyn -> KindM Type
    checkTySynUse tysyn :: TySyn
    tysyn =
        do (ts1 :: [Type]
    ts1,k1 :: Kind
    k1) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts (TySyn -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TySyn
    tysyn)
           let as :: [TParam]
    as  = TySyn -> [TParam]
    tsParams TySyn
    tysyn
           [Type]
    ts2 <- [TParam] -> [Type] -> KindM [Type]
    checkParams [TParam]
    as [Type]
    ts1
           let su :: [(TParam, Type)]
    su = [TParam] -> [Type] -> [(TParam, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TParam]
    as [Type]
    ts2
           [Type]
    ps1 <- (Type -> KindM Type) -> [Type] -> KindM [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Type -> [(TParam, Type)] -> KindM Type
    `kInstantiateT` [(TParam, Type)]
    su) (TySyn -> [Type]
    tsConstraints TySyn
    tysyn)
           ConstraintSource -> [Type] -> KindM ()
    kNewGoals (Name -> ConstraintSource
    CtPartialTypeFun (TySyn -> Name
    tsName TySyn
    tysyn)) [Type]
    ps1
           Type
    t1  <- Type -> [(TParam, Type)] -> KindM Type
    kInstantiateT (TySyn -> Type
    tsDef TySyn
    tysyn) [(TParam, Type)]
    su
           Type -> Maybe Kind -> Kind -> KindM Type
    checkKind (Name -> [Type] -> Type -> Type
    TUser Name
    x [Type]
    ts1 Type
    t1) Maybe Kind
    k Kind
    k1

      checkNewTypeUse :: Newtype -> KindM Type
    checkNewTypeUse nt :: Newtype
    nt =
        do let tc :: TCon
    tc = Newtype -> TCon
    newtypeTyCon Newtype
    nt
           (ts1 :: [Type]
    ts1,_) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc)
           [Type]
    ts2 <- [TParam] -> [Type] -> KindM [Type]
    checkParams (Newtype -> [TParam]
    ntParams Newtype
    nt) [Type]
    ts1
           Type -> KindM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Type] -> Type
    TCon TCon
    tc [Type]
    ts2)

      checkAbstractTypeUse :: AbstractType -> KindM Type
    checkAbstractTypeUse absT :: AbstractType
    absT =
        do let tc :: TCon
    tc   = AbstractType -> TCon
    abstractTypeTC AbstractType
    absT
           (ts1 :: [Type]
    ts1,k1 :: Kind
    k1) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc)
           let (as :: [TParam]
    as,ps :: [Type]
    ps) = AbstractType -> ([TParam], [Type])
    atCtrs AbstractType
    absT
           case [Type]
    ps of
              [] -> () -> KindM ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()   -- common case
              _ -> do let need :: Int
    need = [TParam] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TParam]
    as
                          have :: Int
    have = [Type] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ts1
                      Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    need Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    have) (KindM () -> KindM ()) -> KindM () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $
                         Error -> KindM ()
    kRecordError (Name -> Int -> Error
    TooFewTyParams (AbstractType -> Name
    atName AbstractType
    absT) (Int
    need Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    have))
                      let su :: Subst
    su = [(TVar, Type)] -> Subst
    listSubst ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar [TParam]
    as [TVar] -> [Type] -> [(TVar, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    `zip` [Type]
    ts1)
                      ConstraintSource -> [Type] -> KindM ()
    kNewGoals (Name -> ConstraintSource
    CtPartialTypeFun (AbstractType -> Name
    atName AbstractType
    absT)) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Type -> Type) -> [Type] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Type]
    ps)
           Type -> Maybe Kind -> Kind -> KindM Type
    checkKind (TCon -> [Type] -> Type
    TCon TCon
    tc [Type]
    ts1) Maybe Kind
    k Kind
    k1

      checkParams :: [TParam] -> [Type] -> KindM [Type]
    checkParams as :: [TParam]
    as ts1 :: [Type]
    ts1
        | Int
    paramHave Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    paramNeed = [Type] -> KindM [Type]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Type]
    ts1
        | Int
    paramHave Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    paramNeed  =
                       do Error -> KindM ()
    kRecordError (Name -> Int -> Error
    TooFewTyParams Name
    x (Int
    paramNeedInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    paramHave))
                          let src :: TVarSource
    src = TVarSource
    TypeErrorPlaceHolder
                          [Type]
    fake <- (TParam -> KindM Type) -> [TParam] -> KindM [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (TVarSource -> Kind -> KindM Type
    kNewType TVarSource
    src (Kind -> KindM Type) -> (TParam -> Kind) -> TParam -> KindM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf (TVar -> Kind) -> (TParam -> TVar) -> TParam -> Kind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    tpVar)
                                       (Int -> [TParam] -> [TParam]
    forall a. Int -> [a] -> [a]
    drop Int
    paramHave [TParam]
    as)
                          [Type] -> KindM [Type]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type]
    ts1 [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ [Type]
    fake)
        | Bool
    otherwise = do Error -> KindM ()
    kRecordError (Name -> Int -> Error
    TooManyTySynParams Name
    x (Int
    paramHaveInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    paramNeed))
                         [Type] -> KindM [Type]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> [Type] -> [Type]
    forall a. Int -> [a] -> [a]
    take Int
    paramNeed [Type]
    ts1)
        where paramHave :: Int
    paramHave = [Type] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ts1
              paramNeed :: Int
    paramNeed = [TParam] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TParam]
    as

      checkModuleParamUse :: ModTParam -> KindM Type
    checkModuleParamUse a :: ModTParam
    a =
        do let ty :: TVar
    ty = TParam -> TVar
    tpVar (ModTParam -> TParam
    mtpParam ModTParam
    a)
           (ts1 :: [Type]
    ts1,k1 :: Kind
    k1) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts (TVar -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TVar
    ty)
           case Maybe Kind
    k of
             Just ks :: Kind
    ks | Kind
    ks Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    k1 -> Error -> KindM ()
    kRecordError (Error -> KindM ()) -> Error -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch Kind
    ks Kind
    k1
             _ -> () -> KindM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

           Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Type] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type]
    ts1) (KindM () -> KindM ()) -> KindM () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $
             String -> [String] -> KindM ()
    forall a. HasCallStack => String -> [String] -> a
    panic "Kind.checkTUser.checkModuleParam" [ "Unexpected parameters" ]

           Type -> KindM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar -> Type
    TVar TVar
    ty)

      checkBoundVarUse :: LkpTyVar -> KindM Type
    checkBoundVarUse v :: LkpTyVar
    v =
        do Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Type Name] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type Name]
    ts) (KindM () -> KindM ()) -> KindM () -> KindM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> KindM ()
    kRecordError Error
    TyVarWithParams
           case LkpTyVar
    v of
             TLocalVar t :: TParam
    t mbk :: Maybe Kind
    mbk ->
                case Maybe Kind
    k of
                  Nothing -> Type -> KindM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar -> Type
    TVar (TParam -> TVar
    tpVar TParam
    t))
                  Just k1 :: Kind
    k1 ->
                    case Maybe Kind
    mbk of
                      Nothing -> Name -> Kind -> KindM ()
    kSetKind Name
    x Kind
    k1 KindM () -> KindM Type -> KindM Type
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Type -> KindM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar -> Type
    TVar (TParam -> TVar
    tpVar TParam
    t))
                      Just k2 :: Kind
    k2 -> Type -> Maybe Kind -> Kind -> KindM Type
    checkKind (TVar -> Type
    TVar (TParam -> TVar
    tpVar TParam
    t)) Maybe Kind
    k Kind
    k2
             TOuterVar t :: TParam
    t -> Type -> Maybe Kind -> Kind -> KindM Type
    checkKind (TVar -> Type
    TVar (TParam -> TVar
    tpVar TParam
    t)) Maybe Kind
    k (TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    t)

      checkScopedVarUse :: KindM Type
    checkScopedVarUse =
        do Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Type Name] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type Name]
    ts) (Error -> KindM ()
    kRecordError Error
    TyVarWithParams)
           Name -> Kind -> KindM Type
    kExistTVar Name
    x (Kind -> KindM Type) -> Kind -> KindM Type
    forall a b. (a -> b) -> a -> b
    $ Kind -> Maybe Kind -> Kind
    forall a. a -> Maybe a -> a
    fromMaybe Kind
    KNum Maybe Kind
    k

      mcase :: (Name -> KindM (Maybe a)) ->
               (a -> KindM Type) ->
               KindM Type ->
               KindM Type
      mcase :: (Name -> KindM (Maybe a))
    -> (a -> KindM Type) -> KindM Type -> KindM Type
    mcase m :: Name -> KindM (Maybe a)
    m f :: a -> KindM Type
    f rest :: KindM Type
    rest =
        do Maybe a
    mb <- Name -> KindM (Maybe a)
    m Name
    x
           case Maybe a
    mb of
             Nothing -> KindM Type
    rest
             Just a :: a
    a  -> a -> KindM Type
    f a
    a

    -- | Check a type-application.
    appTy :: [P.Type Name]        -- ^ Parameters to type function
          -> Kind                 -- ^ Kind of type function
          -> KindM ([Type], Kind) -- ^ Validated parameters, resulting kind
    appTy :: [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [] k1 :: Kind
    k1 = ([Type], Kind) -> KindM ([Type], Kind)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([],Kind
    k1)

    appTy (t :: Type Name
    t : ts :: [Type Name]
    ts) (k1 :: Kind
    k1 :-> k2 :: Kind
    k2) =
      do Type
    t1      <- Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    k1)
         (ts1 :: [Type]
    ts1,k :: Kind
    k) <- [Type Name] -> Kind -> KindM ([Type], Kind)
    appTy [Type Name]
    ts Kind
    k2
         ([Type], Kind) -> KindM ([Type], Kind)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    t1 Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    ts1, Kind
    k)

    appTy ts :: [Type Name]
    ts k1 :: Kind
    k1 =
      do Error -> KindM ()
    kRecordError (Int -> Kind -> Error
    TooManyTypeParams ([Type Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type Name]
    ts) Kind
    k1)
         ([Type], Kind) -> KindM ([Type], Kind)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], Kind
    k1)

    -- | Validate a parsed type.
    doCheckType :: P.Type Name  -- ^ Type that needs to be checked
              -> Maybe Kind     -- ^ Expected kind (if any)
              -> KindM Type     -- ^ Checked type
    doCheckType :: Type Name -> Maybe Kind -> KindM Type
    doCheckType ty :: Type Name
    ty k :: Maybe Kind
    k =
      case Type Name
    ty of
        P.TWild         ->
          do AllowWildCards
    wildOk <- KindM AllowWildCards
    kWildOK
             case AllowWildCards
    wildOk of
               AllowWildCards -> () -> KindM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
               NoWildCards    -> Error -> KindM ()
    kRecordError Error
    UnexpectedTypeWildCard
             Kind
    theKind <- case Maybe Kind
    k of
                          Just k1 :: Kind
    k1 -> Kind -> KindM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k1
                          Nothing -> do Warning -> KindM ()
    kRecordWarning (Kind -> Warning
    DefaultingWildType Kind
    P.KNum)
                                        Kind -> KindM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KNum
             TVarSource -> Kind -> KindM Type
    kNewType TVarSource
    TypeWildCard Kind
    theKind

        P.TFun t1 :: Type Name
    t1 t2 :: Type Name
    t2    -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC TC
    TCFun)                 [Type Name
    t1,Type Name
    t2] Maybe Kind
    k
        P.TSeq t1 :: Type Name
    t1 t2 :: Type Name
    t2    -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC TC
    TCSeq)                 [Type Name
    t1,Type Name
    t2] Maybe Kind
    k
        P.TBit          -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC TC
    TCBit)                 [] Maybe Kind
    k
        P.TNum n :: Integer
    n        -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC (Integer -> TC
    TCNum Integer
    n))             [] Maybe Kind
    k
        P.TChar n :: Char
    n       -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC (Integer -> TC
    TCNum (Integer -> TC) -> Integer -> TC
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    n)) [] Maybe Kind
    k

        P.TTuple ts :: [Type Name]
    ts     -> TCon -> [Type Name] -> Maybe Kind -> KindM Type
    tcon (TC -> TCon
    TC (Int -> TC
    TCTuple ([Type Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type Name]
    ts))) [Type Name]
    ts Maybe Kind
    k

        P.TRecord fs :: [Named (Type Name)]
    fs    -> do Type
    t1 <- [(Ident, Type)] -> Type
    TRec ([(Ident, Type)] -> Type) -> KindM [(Ident, Type)] -> KindM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (Named (Type Name) -> KindM (Ident, Type))
    -> [Named (Type Name)] -> KindM [(Ident, Type)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Named (Type Name) -> KindM (Ident, Type)
    checkF [Named (Type Name)]
    fs
                              Type -> Maybe Kind -> Kind -> KindM Type
    checkKind Type
    t1 Maybe Kind
    k Kind
    KType
        P.TLocated t :: Type Name
    t r1 :: Range
    r1 -> Range -> KindM Type -> KindM Type
    forall a. Range -> KindM a -> KindM a
    kInRange Range
    r1 (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t Maybe Kind
    k

        P.TUser x :: Name
    x ts :: [Type Name]
    ts    -> Name -> [Type Name] -> Maybe Kind -> KindM Type
    checkTUser Name
    x [Type Name]
    ts Maybe Kind
    k

        P.TParens t :: Type Name
    t     -> Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t Maybe Kind
    k

        P.TInfix t :: Type Name
    t x :: Located Name
    x _ u :: Type Name
    u-> Type Name -> Maybe Kind -> KindM Type
    doCheckType (Name -> [Type Name] -> Type Name
    forall n. n -> [Type n] -> Type n
    P.TUser (Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x) [Type Name
    t, Type Name
    u]) Maybe Kind
    k

      where
      checkF :: Named (Type Name) -> KindM (Ident, Type)
    checkF f :: Named (Type Name)
    f = do Type
    t <- Range -> KindM Type -> KindM Type
    forall a. Range -> KindM a -> KindM a
    kInRange (Located Ident -> Range
    forall a. Located a -> Range
    srcRange (Named (Type Name) -> Located Ident
    forall a. Named a -> Located Ident
    name Named (Type Name)
    f))
                       (KindM Type -> KindM Type) -> KindM Type -> KindM Type
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Type
    doCheckType (Named (Type Name) -> Type Name
    forall a. Named a -> a
    value Named (Type Name)
    f) (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)
                    (Ident, Type) -> KindM (Ident, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Located Ident -> Ident
    forall a. Located a -> a
    thing (Named (Type Name) -> Located Ident
    forall a. Named a -> Located Ident
    name Named (Type Name)
    f), Type
    t)

    -- | Validate a parsed proposition.
    checkProp :: P.Prop Name      -- ^ Proposition that need to be checked
              -> KindM Type       -- ^ Checked representation
    checkProp :: Prop Name -> KindM Type
    checkProp (P.CType t :: Type Name
    t) = Type Name -> Maybe Kind -> KindM Type
    doCheckType Type Name
    t (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KProp)

    -- | Check that a type has the expected kind.
    checkKind :: Type         -- ^ Kind-checked type
              -> Maybe Kind   -- ^ Expected kind (if any)
              -> Kind         -- ^ Inferred kind
              -> KindM Type   -- ^ A type consistent with expectations.
    checkKind :: Type -> Maybe Kind -> Kind -> KindM Type
    checkKind _ (Just k1 :: Kind
    k1) k2 :: Kind
    k2
      | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    k2    = do Error -> KindM ()
    kRecordError (Kind -> Kind -> Error
    KindMismatch Kind
    k1 Kind
    k2)
                         TVarSource -> Kind -> KindM Type
    kNewType TVarSource
    TypeErrorPlaceHolder Kind
    k1
    checkKind t :: Type
    t _ _ = Type -> KindM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t