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

    {-# LANGUAGE RecursiveDo #-}
    {-# LANGUAGE BlockArguments #-}
    -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    module Cryptol.TypeCheck.Kind
      ( checkType
      , checkSchema
      , checkNewtype
      , checkPrimType
      , checkTySyn
      , checkPropSyn
      , checkParameterType
      , checkParameterConstraints
      , checkPropGuards
      ) where

    import qualified Cryptol.Parser.AST as P
    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           Cryptol.Utils.RecordMap

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

    -- | 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 AllowWildCards
    withWild (P.Forall [TParam Name]
    xs [Prop Name]
    ps Type Name
    t Maybe Range
    mb) =
      do (([TParam]
    xs1,([Prop]
    ps1,Prop
    t1)), [Goal]
    gs) <-
            InferM ([TParam], ([Prop], Prop))
    -> InferM (([TParam], ([Prop], Prop)), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals (InferM ([TParam], ([Prop], Prop))
     -> InferM (([TParam], ([Prop], Prop)), [Goal]))
    -> InferM ([TParam], ([Prop], Prop))
    -> InferM (([TParam], ([Prop], Prop)), [Goal])
    forall a b. (a -> b) -> a -> b
    $
            InferM ([TParam], ([Prop], Prop))
    -> InferM ([TParam], ([Prop], Prop))
    forall {a}. InferM a -> InferM a
    rng (InferM ([TParam], ([Prop], Prop))
     -> InferM ([TParam], ([Prop], Prop)))
    -> InferM ([TParam], ([Prop], Prop))
    -> InferM ([TParam], ([Prop], Prop))
    forall a b. (a -> b) -> a -> b
    $ AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM ([Prop], Prop)
    -> InferM ([TParam], ([Prop], Prop))
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    withWild Name -> TPFlavor
    schemaParam [TParam Name]
    xs (KindM ([Prop], Prop) -> InferM ([TParam], ([Prop], Prop)))
    -> KindM ([Prop], Prop) -> InferM ([TParam], ([Prop], Prop))
    forall a b. (a -> b) -> a -> b
    $
            do [Prop]
    ps1 <- (Prop Name -> KindM Prop) -> [Prop Name] -> KindM [Prop]
    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 Prop Name -> KindM Prop
    checkProp [Prop Name]
    ps
               Prop
    t1  <- Type Name -> Maybe Kind -> KindM Prop
    doCheckType Type Name
    t (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)
               ([Prop], Prop) -> KindM ([Prop], Prop)
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Prop]
    ps1,Prop
    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 :: [Prop]
    newPs = (Prop -> [Prop]) -> [Prop] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Prop -> [Prop]
    pSplitAnd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> a -> b
    $ (Prop -> Prop) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ctxt -> Prop -> Prop
    simplify Ctxt
    forall a. Monoid a => a
    mempty)
                                         ([Prop] -> [Prop]) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> a -> b
    $ (Prop -> Prop) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Prop
    tRebuild [Prop]
    ps1
         (Schema, [Goal]) -> InferM (Schema, [Goal])
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( [TParam] -> [Prop] -> Prop -> Schema
    Forall [TParam]
    xs1 [Prop]
    newPs (Prop -> Prop
    tRebuild Prop
    t1)
                , [ Goal
    g { goal :: Prop
    goal = Prop -> Prop
    tRebuild (Goal -> Prop
    goal Goal
    g) } | Goal
    g <- [Goal]
    gs ]
                )

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

    {- | Validate parsed propositions that appear in the guard of a PropGuard.

      * Note that we don't validate the well-formedness constraints here---instead,
        they'd be validated when the signature for the auto generated
        function corresponding guard is checked.

      * We also check that there are no wild-cards in the constraints.
    -}
    checkPropGuards :: [Located (P.Prop Name)] -> InferM [Prop]
    checkPropGuards :: [Located (Prop Name)] -> InferM [Prop]
    checkPropGuards [Located (Prop Name)]
    props =
      do ([Prop]
    newPs,[Goal]
    _gs) <- InferM [Prop] -> InferM ([Prop], [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals ((Located (Prop Name) -> InferM Prop)
    -> [Located (Prop Name)] -> InferM [Prop]
    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 Located (Prop Name) -> InferM Prop
    check [Located (Prop Name)]
    props)
         [Prop] -> InferM [Prop]
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Prop]
    newPs
      where
      check :: Located (Prop Name) -> InferM Prop
    check Located (Prop Name)
    lp =
        Range -> InferM Prop -> InferM Prop
    forall a. Range -> InferM a -> InferM a
    inRange (Located (Prop Name) -> Range
    forall a. Located a -> Range
    srcRange Located (Prop Name)
    lp)
        do let p :: Prop Name
    p = Located (Prop Name) -> Prop Name
    forall a. Located a -> a
    thing Located (Prop Name)
    lp
           ([TParam]
    _,Prop
    ps) <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM Prop
    -> InferM ([TParam], Prop)
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    schemaParam [] (Prop Name -> KindM Prop
    checkProp Prop Name
    p)
           case Prop -> Prop
    tNoUser Prop
    ps of
             TCon (PC PC
    x) [Prop]
    _ | PC
    x PC -> [PC] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [PC
    PEqual,PC
    PNeq,PC
    PGeq,PC
    PFin,PC
    PTrue] -> () -> InferM ()
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
             Prop
    _ -> Error -> InferM ()
    recordError (Prop -> Error
    InvalidConstraintGuard Prop
    ps)
           Prop -> InferM Prop
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Prop
    ps

    -- | Check a module parameter declarations.  Nothing much to check,
    -- we just translate from one syntax to another.
    checkParameterType :: P.ParameterType Name -> InferM ModTParam
    checkParameterType :: ParameterType Name -> InferM ModTParam
    checkParameterType ParameterType Name
    a =
      do let mbDoc :: Maybe Text
    mbDoc = ParameterType Name -> Maybe Text
    forall name. ParameterType name -> Maybe Text
    P.ptDoc ParameterType Name
    a
             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 a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModTParam { mtpKind :: Kind
    mtpKind = Kind
    k, mtpName :: Name
    mtpName = Name
    n, mtpDoc :: Maybe Text
    mtpDoc = Maybe Text
    mbDoc }

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

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

    -- | Check a newtype declaration.
    -- XXX: Do something with constraints.
    checkNewtype :: P.Newtype Name -> Maybe Text -> InferM Newtype
    checkNewtype :: Newtype Name -> Maybe Text -> InferM Newtype
    checkNewtype (P.Newtype Located Name
    x [TParam Name]
    as Name
    con Rec (Type Name)
    fs) Maybe Text
    mbD =
      do (([TParam]
    as1,RecordMap Ident Prop
    fs1),[Goal]
    gs) <- InferM ([TParam], RecordMap Ident Prop)
    -> InferM (([TParam], RecordMap Ident Prop), [Goal])
    forall a. InferM a -> InferM (a, [Goal])
    collectGoals (InferM ([TParam], RecordMap Ident Prop)
     -> InferM (([TParam], RecordMap Ident Prop), [Goal]))
    -> InferM ([TParam], RecordMap Ident Prop)
    -> InferM (([TParam], RecordMap Ident Prop), [Goal])
    forall a b. (a -> b) -> a -> b
    $
           Range
    -> InferM ([TParam], RecordMap Ident Prop)
    -> InferM ([TParam], RecordMap Ident Prop)
    forall a. Range -> InferM a -> InferM a
    inRange (Located Name -> Range
    forall a. Located a -> Range
    srcRange Located Name
    x) (InferM ([TParam], RecordMap Ident Prop)
     -> InferM ([TParam], RecordMap Ident Prop))
    -> InferM ([TParam], RecordMap Ident Prop)
    -> InferM ([TParam], RecordMap Ident Prop)
    forall a b. (a -> b) -> a -> b
    $
           do ([TParam], RecordMap Ident Prop)
    r <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM (RecordMap Ident Prop)
    -> InferM ([TParam], RecordMap Ident Prop)
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    newtypeParam [TParam Name]
    as (KindM (RecordMap Ident Prop)
     -> InferM ([TParam], RecordMap Ident Prop))
    -> KindM (RecordMap Ident Prop)
    -> InferM ([TParam], RecordMap Ident Prop)
    forall a b. (a -> b) -> a -> b
    $
                   ((Ident -> (Range, Type Name) -> KindM Prop)
     -> Rec (Type Name) -> KindM (RecordMap Ident Prop))
    -> Rec (Type Name)
    -> (Ident -> (Range, Type Name) -> KindM Prop)
    -> KindM (RecordMap Ident Prop)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Ident -> (Range, Type Name) -> KindM Prop)
    -> Rec (Type Name) -> KindM (RecordMap Ident Prop)
    forall (t :: * -> *) a b c.
    Applicative t =>
    (a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
    traverseRecordMap Rec (Type Name)
    fs ((Ident -> (Range, Type Name) -> KindM Prop)
     -> KindM (RecordMap Ident Prop))
    -> (Ident -> (Range, Type Name) -> KindM Prop)
    -> KindM (RecordMap Ident Prop)
    forall a b. (a -> b) -> a -> b
    $ \Ident
    _n (Range
    rng,Type Name
    f) ->
                     Range -> KindM Prop -> KindM Prop
    forall a. Range -> KindM a -> KindM a
    kInRange Range
    rng (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Prop
    doCheckType Type Name
    f (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)
              InferM ()
    simplifyAllConstraints
              ([TParam], RecordMap Ident Prop)
    -> InferM ([TParam], RecordMap Ident Prop)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam], RecordMap Ident Prop)
    r

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

    checkPrimType :: P.PrimType Name -> Maybe Text -> InferM AbstractType
    checkPrimType :: PrimType Name -> Maybe Text -> InferM AbstractType
    checkPrimType PrimType Name
    p Maybe Text
    mbD =
      do let ([TParam Name]
    as,[Prop Name]
    cs) = PrimType Name -> ([TParam Name], [Prop Name])
    forall name. PrimType name -> ([TParam name], [Prop name])
    P.primTCts PrimType Name
    p
         ([TParam]
    as',[Prop]
    cs') <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [Prop]
    -> InferM ([TParam], [Prop])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    TPPrimParam [TParam Name]
    as (KindM [Prop] -> InferM ([TParam], [Prop]))
    -> KindM [Prop] -> InferM ([TParam], [Prop])
    forall a b. (a -> b) -> a -> b
    $
                        (Prop Name -> KindM Prop) -> [Prop Name] -> KindM [Prop]
    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 Prop Name -> KindM Prop
    checkProp [Prop Name]
    cs
         AbstractType -> InferM AbstractType
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure 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], [Prop])
    atCtrs = ([TParam]
    as',[Prop]
    cs')
                           , atDoc :: Maybe Text
    atDoc = Maybe Text
    mbD
                           }

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

    checkParameterConstraints :: [Located (P.Prop Name)] -> InferM [Located Prop]
    checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop]
    checkParameterConstraints [Located (Prop Name)]
    ps =
      do ([TParam]
    _, [Located Prop]
    cs) <- AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM [Located Prop]
    -> InferM ([TParam], [Located Prop])
    forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    NoWildCards Name -> TPFlavor
    schemaParam [] ((Located (Prop Name) -> KindM (Located Prop))
    -> [Located (Prop Name)] -> KindM [Located Prop]
    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 Located (Prop Name) -> KindM (Located Prop)
    checkL [Located (Prop Name)]
    ps)
         [Located Prop] -> InferM [Located Prop]
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Located Prop]
    cs
      where
      checkL :: Located (Prop Name) -> KindM (Located Prop)
    checkL Located (Prop Name)
    x = do Prop
    p <- Prop Name -> KindM Prop
    checkProp (Located (Prop Name) -> Prop Name
    forall a. Located a -> a
    thing Located (Prop Name)
    x)
                    Located Prop -> KindM (Located Prop)
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Located (Prop Name)
    x { thing :: Prop
    thing = Prop -> Prop
    tRebuild Prop
    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 :: forall a.
    AllowWildCards
    -> (Name -> TPFlavor)
    -> [TParam Name]
    -> KindM a
    -> InferM ([TParam], a)
    withTParams AllowWildCards
    allowWildCards Name -> TPFlavor
    flav [TParam Name]
    xs KindM a
    m
      | Bool -> Bool
    not ([[TParam Name]] -> Bool
    forall a. [a] -> 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 String
    "withTParams" ([String] -> InferM ([TParam], a))
    -> [String] -> InferM ([TParam], a)
    forall a b. (a -> b) -> a -> b
    $ String
    "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 ([TParam]
    as,a
    a,[(ConstraintSource, [Prop])]
    ctrs) <-
            mdo (a
    a, Map Name Kind
    vars,[(ConstraintSource, [Prop])]
    ctrs) <- AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
    forall a.
    AllowWildCards
    -> [(Name, Maybe Kind, TParam)]
    -> KindM a
    -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Map Name Kind -> TParam Name -> InferM TParam
    newTP Map Name Kind
    vars) [TParam Name]
    xs
                ([TParam], a, [(ConstraintSource, [Prop])])
    -> InferM ([TParam], a, [(ConstraintSource, [Prop])])
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam]
    as,a
    a,[(ConstraintSource, [Prop])]
    ctrs)
         ((ConstraintSource, [Prop]) -> InferM ())
    -> [(ConstraintSource, [Prop])] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((ConstraintSource -> [Prop] -> InferM ())
    -> (ConstraintSource, [Prop]) -> InferM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ConstraintSource -> [Prop] -> InferM ()
    newGoals) [(ConstraintSource, [Prop])]
    ctrs
         ([TParam], a) -> InferM ([TParam], a)
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam]
    as,a
    a)

      where
      getKind :: Map Name Kind -> TParam Name -> InferM Kind
    getKind Map Name Kind
    vs 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 Kind
    k  -> Kind -> InferM Kind
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
          Maybe Kind
    Nothing -> do Warning -> InferM ()
    recordWarning (TParam Name -> Kind -> Warning
    DefaultingKind TParam Name
    tp Kind
    P.KNum)
                        Kind -> InferM Kind
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KNum

      newTP :: Map Name Kind -> TParam Name -> InferM TParam
    newTP Map Name Kind
    vs 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' [] [c]
    _           = []
      zip' (TParam n
    a:[TParam n]
    as) ~(c
    t:[c]
    ts) = (TParam n -> n
    forall n. TParam n -> n
    P.tpName TParam n
    a, (Kind -> Kind) -> Maybe Kind -> Maybe Kind
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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
    _ : [TParam Name]
    _) <- (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 Kind
    P.KNum  = Kind
    KNum
    cvtK Kind
    P.KType = Kind
    KType
    cvtK Kind
    P.KProp = Kind
    KProp
    cvtK (P.KFun Kind
    k1 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 Prop
    tcon TCon
    tc [Type Name]
    ts0 Maybe Kind
    k =
      do ([Prop]
    ts1,Kind
    k1) <- [Type Name] -> Kind -> KindM ([Prop], Kind)
    appTy [Type Name]
    ts0 (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc)
         Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind (TCon -> [Prop] -> Prop
    TCon TCon
    tc [Prop]
    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 Prop
    checkTUser Name
    x [Type Name]
    ts Maybe Kind
    k =
      (Name -> KindM (Maybe LkpTyVar))
    -> (LkpTyVar -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe LkpTyVar)
    kLookupTyVar      LkpTyVar -> KindM Prop
    checkBoundVarUse (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe TySyn))
    -> (TySyn -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe TySyn)
    kLookupTSyn       TySyn -> KindM Prop
    checkTySynUse (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe Newtype))
    -> (Newtype -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe Newtype)
    kLookupNewtype    Newtype -> KindM Prop
    checkNewTypeUse (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe ModTParam))
    -> (ModTParam -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe ModTParam)
    kLookupParamType  ModTParam -> KindM Prop
    checkModuleParamUse (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $
      (Name -> KindM (Maybe AbstractType))
    -> (AbstractType -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe AbstractType)
    kLookupAbstractType AbstractType -> KindM Prop
    checkAbstractTypeUse (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $
      KindM Prop
    checkScopedVarUse -- none of the above, must be a scoped type variable,
                        -- if the renamer did its job correctly.
      where
      checkTySynUse :: TySyn -> KindM Prop
    checkTySynUse TySyn
    tysyn =
        do ([Prop]
    ts1,Kind
    k1) <- [Type Name] -> Kind -> KindM ([Prop], 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
           [Prop]
    ts2 <- [TParam] -> [Prop] -> KindM [Prop]
    checkParams [TParam]
    as [Prop]
    ts1
           let su :: [(TParam, Prop)]
    su = [TParam] -> [Prop] -> [(TParam, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TParam]
    as [Prop]
    ts2
           [Prop]
    ps1 <- (Prop -> KindM Prop) -> [Prop] -> KindM [Prop]
    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 (Prop -> [(TParam, Prop)] -> KindM Prop
    `kInstantiateT` [(TParam, Prop)]
    su) (TySyn -> [Prop]
    tsConstraints TySyn
    tysyn)
           ConstraintSource -> [Prop] -> KindM ()
    kNewGoals (Name -> ConstraintSource
    CtPartialTypeFun (TySyn -> Name
    tsName TySyn
    tysyn)) [Prop]
    ps1
           Prop
    t1  <- Prop -> [(TParam, Prop)] -> KindM Prop
    kInstantiateT (TySyn -> Prop
    tsDef TySyn
    tysyn) [(TParam, Prop)]
    su
           Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind (Name -> [Prop] -> Prop -> Prop
    TUser Name
    x [Prop]
    ts1 Prop
    t1) Maybe Kind
    k Kind
    k1

      checkNewTypeUse :: Newtype -> KindM Prop
    checkNewTypeUse Newtype
    nt =
        do ([Prop]
    ts1,Kind
    k1) <- [Type Name] -> Kind -> KindM ([Prop], Kind)
    appTy [Type Name]
    ts (Newtype -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Newtype
    nt)
           let as :: [TParam]
    as = Newtype -> [TParam]
    ntParams Newtype
    nt
           [Prop]
    ts2 <- [TParam] -> [Prop] -> KindM [Prop]
    checkParams [TParam]
    as [Prop]
    ts1
           let su :: [(TParam, Prop)]
    su = [TParam] -> [Prop] -> [(TParam, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TParam]
    as [Prop]
    ts2
           [Prop]
    ps1 <- (Prop -> KindM Prop) -> [Prop] -> KindM [Prop]
    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 (Prop -> [(TParam, Prop)] -> KindM Prop
    `kInstantiateT` [(TParam, Prop)]
    su) (Newtype -> [Prop]
    ntConstraints Newtype
    nt)
           ConstraintSource -> [Prop] -> KindM ()
    kNewGoals (Name -> ConstraintSource
    CtPartialTypeFun (Newtype -> Name
    ntName Newtype
    nt)) [Prop]
    ps1
           Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind (Newtype -> [Prop] -> Prop
    TNewtype Newtype
    nt [Prop]
    ts2) Maybe Kind
    k Kind
    k1

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

      checkParams :: [TParam] -> [Prop] -> KindM [Prop]
    checkParams [TParam]
    as [Prop]
    ts1
        | Int
    paramHave Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    paramNeed = [Prop] -> KindM [Prop]
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Prop]
    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 :: TypeSource
    src = TypeSource
    TypeErrorPlaceHolder
                          [Prop]
    fake <- (TParam -> KindM Prop) -> [TParam] -> KindM [Prop]
    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 (TypeSource -> Kind -> KindM Prop
    kNewType TypeSource
    src (Kind -> KindM Prop) -> (TParam -> Kind) -> TParam -> KindM Prop
    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)
                          [Prop] -> KindM [Prop]
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Prop]
    ts1 [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    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))
                         [Prop] -> KindM [Prop]
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> [Prop] -> [Prop]
    forall a. Int -> [a] -> [a]
    take Int
    paramNeed [Prop]
    ts1)
        where paramHave :: Int
    paramHave = [Prop] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Prop]
    ts1
              paramNeed :: Int
    paramNeed = [TParam] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TParam]
    as

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

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

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

      checkBoundVarUse :: LkpTyVar -> KindM Prop
    checkBoundVarUse LkpTyVar
    v =
        do Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Type Name] -> Bool
    forall a. [a] -> 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 TParam
    t Maybe Kind
    mbk ->
                case Maybe Kind
    k of
                  Maybe Kind
    Nothing -> Prop -> KindM Prop
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar -> Prop
    TVar (TParam -> TVar
    tpVar TParam
    t))
                  Just Kind
    k1 ->
                    case Maybe Kind
    mbk of
                      Maybe Kind
    Nothing -> Name -> Kind -> KindM ()
    kSetKind Name
    x Kind
    k1 KindM () -> KindM Prop -> KindM Prop
    forall a b. KindM a -> KindM b -> KindM b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Prop -> KindM Prop
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar -> Prop
    TVar (TParam -> TVar
    tpVar TParam
    t))
                      Just Kind
    k2 -> Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind (TVar -> Prop
    TVar (TParam -> TVar
    tpVar TParam
    t)) Maybe Kind
    k Kind
    k2
             TOuterVar TParam
    t -> Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind (TVar -> Prop
    TVar (TParam -> TVar
    tpVar TParam
    t)) Maybe Kind
    k (TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    t)

      checkScopedVarUse :: KindM Prop
    checkScopedVarUse =
        do Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Type Name] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type Name]
    ts) (Error -> KindM ()
    kRecordError Error
    TyVarWithParams)
           Name -> Kind -> KindM Prop
    kExistTVar Name
    x (Kind -> KindM Prop) -> Kind -> KindM Prop
    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 :: forall a.
    (Name -> KindM (Maybe a))
    -> (a -> KindM Prop) -> KindM Prop -> KindM Prop
    mcase Name -> KindM (Maybe a)
    m a -> KindM Prop
    f KindM Prop
    rest =
        do Maybe a
    mb <- Name -> KindM (Maybe a)
    m Name
    x
           case Maybe a
    mb of
             Maybe a
    Nothing -> KindM Prop
    rest
             Just a
    a  -> a -> KindM Prop
    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 ([Prop], Kind)
    appTy [] Kind
    k1 = ([Prop], Kind) -> KindM ([Prop], Kind)
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([],Kind
    k1)

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

    appTy [Type Name]
    ts Kind
    k1 =
      do Error -> KindM ()
    kRecordError (Int -> Kind -> Error
    TooManyTypeParams ([Type Name] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type Name]
    ts) Kind
    k1)
         ([Prop], Kind) -> KindM ([Prop], Kind)
    forall a. a -> KindM a
    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 Prop
    doCheckType Type Name
    ty Maybe Kind
    k =
      case Type Name
    ty of
        Type Name
    P.TWild         ->
          do AllowWildCards
    wildOk <- KindM AllowWildCards
    kWildOK
             case AllowWildCards
    wildOk of
               AllowWildCards
    AllowWildCards -> () -> KindM ()
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
               AllowWildCards
    NoWildCards    -> Error -> KindM ()
    kRecordError Error
    UnexpectedTypeWildCard
             Kind
    theKind <- case Maybe Kind
    k of
                          Just Kind
    k1 -> Kind -> KindM Kind
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k1
                          Maybe Kind
    Nothing -> do Warning -> KindM ()
    kRecordWarning (Kind -> Warning
    DefaultingWildType Kind
    P.KNum)
                                        Kind -> KindM Kind
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KNum
             TypeSource -> Kind -> KindM Prop
    kNewType TypeSource
    TypeWildCard Kind
    theKind

        P.TFun Type Name
    t1 Type Name
    t2    -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    tcon (TC -> TCon
    TC TC
    TCFun)                 [Type Name
    t1,Type Name
    t2] Maybe Kind
    k
        P.TSeq Type Name
    t1 Type Name
    t2    -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    tcon (TC -> TCon
    TC TC
    TCSeq)                 [Type Name
    t1,Type Name
    t2] Maybe Kind
    k
        Type Name
    P.TBit          -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    tcon (TC -> TCon
    TC TC
    TCBit)                 [] Maybe Kind
    k
        P.TNum Integer
    n        -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    tcon (TC -> TCon
    TC (Integer -> TC
    TCNum Integer
    n))             [] Maybe Kind
    k
        P.TChar Char
    n       -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    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 [Type Name]
    ts     -> TCon -> [Type Name] -> Maybe Kind -> KindM Prop
    tcon (TC -> TCon
    TC (Int -> TC
    TCTuple ([Type Name] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type Name]
    ts))) [Type Name]
    ts Maybe Kind
    k

        P.TRecord Rec (Type Name)
    fs    -> do Prop
    t1 <- RecordMap Ident Prop -> Prop
    TRec (RecordMap Ident Prop -> Prop)
    -> KindM (RecordMap Ident Prop) -> KindM Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Ident -> (Range, Type Name) -> KindM Prop)
    -> Rec (Type Name) -> KindM (RecordMap Ident Prop)
    forall (t :: * -> *) a b c.
    Applicative t =>
    (a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
    traverseRecordMap Ident -> (Range, Type Name) -> KindM Prop
    forall {p}. p -> (Range, Type Name) -> KindM Prop
    checkF Rec (Type Name)
    fs
                              Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind Prop
    t1 Maybe Kind
    k Kind
    KType
        P.TLocated Type Name
    t Range
    r1 -> Range -> KindM Prop -> KindM Prop
    forall a. Range -> KindM a -> KindM a
    kInRange Range
    r1 (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Prop
    doCheckType Type Name
    t Maybe Kind
    k

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

        P.TParens Type Name
    t Maybe Kind
    mb  ->
          do Maybe Kind
    newK <- case (Maybe Kind
    k, Kind -> Kind
    cvtK (Kind -> Kind) -> Maybe Kind -> Maybe Kind
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Kind
    mb) of
                       (Just Kind
    a, Just Kind
    b) ->
                          do Bool -> KindM () -> KindM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Kind
    a Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    b)
                               (Error -> KindM ()
    kRecordError (Maybe TypeSource -> Kind -> Kind -> Error
    KindMismatch Maybe TypeSource
    forall a. Maybe a
    Nothing Kind
    a Kind
    b))
                             Maybe Kind -> KindM (Maybe Kind)
    forall a. a -> KindM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    b)
                       (Maybe Kind
    a,Maybe Kind
    b) -> Maybe Kind -> KindM (Maybe Kind)
    forall a. a -> KindM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe Kind -> Maybe Kind -> Maybe Kind
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus Maybe Kind
    a Maybe Kind
    b)

             Type Name -> Maybe Kind -> KindM Prop
    doCheckType Type Name
    t Maybe Kind
    newK

        P.TInfix Type Name
    t Located Name
    x Fixity
    _ Type Name
    u-> Type Name -> Maybe Kind -> KindM Prop
    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

        P.TTyApp [Named (Type Name)]
    _fs    -> do Error -> KindM ()
    kRecordError Error
    BareTypeApp
                              TypeSource -> Kind -> KindM Prop
    kNewType TypeSource
    TypeWildCard Kind
    KNum

      where
      checkF :: p -> (Range, Type Name) -> KindM Prop
    checkF p
    _nm (Range
    rng,Type Name
    v) = Range -> KindM Prop -> KindM Prop
    forall a. Range -> KindM a -> KindM a
    kInRange Range
    rng (KindM Prop -> KindM Prop) -> KindM Prop -> KindM Prop
    forall a b. (a -> b) -> a -> b
    $ Type Name -> Maybe Kind -> KindM Prop
    doCheckType Type Name
    v (Kind -> Maybe Kind
    forall a. a -> Maybe a
    Just Kind
    KType)

    -- | Validate a parsed proposition.
    checkProp :: P.Prop Name      -- ^ Proposition that need to be checked
              -> KindM Prop -- ^ Checked representation
    checkProp :: Prop Name -> KindM Prop
    checkProp (P.CType Type Name
    t) = Type Name -> Maybe Kind -> KindM Prop
    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 :: Prop -> Maybe Kind -> Kind -> KindM Prop
    checkKind Prop
    _ (Just Kind
    k1) Kind
    k2
      | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    k2    = do Error -> KindM ()
    kRecordError (Maybe TypeSource -> Kind -> Kind -> Error
    KindMismatch Maybe TypeSource
    forall a. Maybe a
    Nothing Kind
    k1 Kind
    k2)
                         TypeSource -> Kind -> KindM Prop
    kNewType TypeSource
    TypeErrorPlaceHolder Kind
    k1
    checkKind Prop
    t Maybe Kind
    _ Kind
    _ = Prop -> KindM Prop
    forall a. a -> KindM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    t