-- |
-- 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
  , checkEnum
  , 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.Subst(listSubst,apSubst)
import           Cryptol.TypeCheck.Monad hiding (withTParams)
import           Cryptol.TypeCheck.SimpType(tRebuild)
import           Cryptol.TypeCheck.SimpleSolver(simplify)
import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)
import           Cryptol.Utils.Panic (panic)
import           Cryptol.Utils.PP(pp,commaSep)
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,mplus,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 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 = tRebuild (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 (Located Text)
mbDoc = ParameterType Name -> Maybe (Located Text)
forall name. ParameterType name -> Maybe (Located 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 = Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Located 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.
checkNewtype :: P.Newtype Name -> Maybe Text -> InferM NominalType
checkNewtype :: Newtype Name -> Maybe Text -> InferM NominalType
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
nominalParam [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

     NominalType -> InferM NominalType
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return NominalType
                    { ntName :: Name
ntName   = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
                    , ntKind :: Kind
ntKind   = Kind
KType
                    , 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
                    , ntDef :: NominalTypeDef
ntDef = StructCon -> NominalTypeDef
Struct
                                StructCon { ntConName :: Name
ntConName = Name
con, ntFields :: RecordMap Ident Prop
ntFields = RecordMap Ident Prop
fs1 }
                    , ntFixity :: Maybe Fixity
ntFixity = Maybe Fixity
forall a. Maybe a
Nothing
                    , ntDoc :: Maybe Text
ntDoc = Maybe Text
mbD
                    }

checkEnum :: P.EnumDecl Name -> Maybe Text -> InferM NominalType
checkEnum :: EnumDecl Name -> Maybe Text -> InferM NominalType
checkEnum EnumDecl Name
ed Maybe Text
mbD =
  do let x :: Located Name
x = EnumDecl Name -> Located Name
forall name. EnumDecl name -> Located name
P.eName EnumDecl Name
ed
     (([TParam]
as1,[EnumCon]
cons1),[Goal]
gs) <- InferM ([TParam], [EnumCon])
-> InferM (([TParam], [EnumCon]), [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM ([TParam], [EnumCon])
 -> InferM (([TParam], [EnumCon]), [Goal]))
-> InferM ([TParam], [EnumCon])
-> InferM (([TParam], [EnumCon]), [Goal])
forall a b. (a -> b) -> a -> b
$
       Range
-> InferM ([TParam], [EnumCon]) -> InferM ([TParam], [EnumCon])
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x) (InferM ([TParam], [EnumCon]) -> InferM ([TParam], [EnumCon]))
-> InferM ([TParam], [EnumCon]) -> InferM ([TParam], [EnumCon])
forall a b. (a -> b) -> a -> b
$
       do ([TParam], [EnumCon])
r <- AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM [EnumCon]
-> InferM ([TParam], [EnumCon])
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards Name -> TPFlavor
nominalParam (EnumDecl Name -> [TParam Name]
forall name. EnumDecl name -> [TParam name]
P.eParams EnumDecl Name
ed) (KindM [EnumCon] -> InferM ([TParam], [EnumCon]))
-> KindM [EnumCon] -> InferM ([TParam], [EnumCon])
forall a b. (a -> b) -> a -> b
$
               [(TopLevel (EnumCon Name), Int)]
-> ((TopLevel (EnumCon Name), Int) -> KindM EnumCon)
-> KindM [EnumCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (EnumDecl Name -> [TopLevel (EnumCon Name)]
forall name. EnumDecl name -> [TopLevel (EnumCon name)]
P.eCons EnumDecl Name
ed [TopLevel (EnumCon Name)]
-> [Int] -> [(TopLevel (EnumCon Name), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0..]) \(TopLevel (EnumCon Name)
tlC,Int
nu) ->
                 do let con :: EnumCon Name
con = TopLevel (EnumCon Name) -> EnumCon Name
forall a. TopLevel a -> a
P.tlValue TopLevel (EnumCon Name)
tlC
                        cname :: Located Name
cname = EnumCon Name -> Located Name
forall name. EnumCon name -> Located name
P.ecName EnumCon Name
con
                    [Prop]
ts <- Range -> KindM [Prop] -> KindM [Prop]
forall a. Range -> KindM a -> KindM a
kInRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
cname)
                            ((Type Name -> KindM Prop) -> [Type 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 (Type Name -> Maybe Kind -> KindM Prop
`doCheckType` Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KType) (EnumCon Name -> [Type Name]
forall name. EnumCon name -> [Type name]
P.ecFields EnumCon Name
con))
                    EnumCon -> KindM EnumCon
forall a. a -> KindM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EnumCon
                          { ecName :: Name
ecName   = Located Name -> Name
forall a. Located a -> a
thing Located Name
cname
                          , ecNumber :: Int
ecNumber = Int
nu
                          , ecFields :: [Prop]
ecFields = [Prop]
ts
                          , ecPublic :: Bool
ecPublic = TopLevel (EnumCon Name) -> ExportType
forall a. TopLevel a -> ExportType
P.tlExport TopLevel (EnumCon Name)
tlC ExportType -> ExportType -> Bool
forall a. Eq a => a -> a -> Bool
== ExportType
P.Public
                          , ecDoc :: Maybe Text
ecDoc    = Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (EnumCon Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (EnumCon Name)
tlC
                          }
          InferM ()
simplifyAllConstraints
          ([TParam], [EnumCon]) -> InferM ([TParam], [EnumCon])
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TParam], [EnumCon])
r
     NominalType -> InferM NominalType
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalType
                  { ntName :: Name
ntName = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
                  , ntParams :: [TParam]
ntParams = [TParam]
as1
                  , ntKind :: Kind
ntKind = Kind
KType
                  , ntConstraints :: [Prop]
ntConstraints = (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
gs
                  , ntDef :: NominalTypeDef
ntDef = [EnumCon] -> NominalTypeDef
Enum [EnumCon]
cons1
                  , ntFixity :: Maybe Fixity
ntFixity = Maybe Fixity
forall a. Maybe a
Nothing
                  , ntDoc :: Maybe Text
ntDoc = Maybe Text
mbD
                  }

checkPrimType :: P.PrimType Name -> Maybe Text -> InferM NominalType
checkPrimType :: PrimType Name -> Maybe Text -> InferM NominalType
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 ((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)
     let ([Kind]
args,Kind
finK) = Kind -> ([Kind], Kind)
splitK (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)))
         ([Kind]
declared,[Kind]
others) = Int -> [Kind] -> ([Kind], [Kind])
forall a. Int -> [a] -> ([a], [a])
splitAt ([TParam] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TParam]
as') [Kind]
args
     Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Kind -> Kind -> Bool) -> [Kind] -> [Kind] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((TParam -> Kind) -> [TParam] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf [TParam]
as') [Kind]
args)) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
       String -> [String] -> InferM ()
forall a. HasCallStack => String -> [String] -> a
panic String
"checkPrimType"
         [ String
"Primtive declaration, kind argument prefix mismach:"
         , String
"Expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ([Doc] -> Doc
commaSep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Kind -> Doc
forall a. PP a => a -> Doc
pp (Kind -> Doc) -> (TParam -> Kind) -> TParam -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf) [TParam]
as'))
         , String
"Actual: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ([Doc] -> Doc
commaSep ((Kind -> Doc) -> [Kind] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> Doc
forall a. PP a => a -> Doc
pp [Kind]
declared))
         ]
     NominalType -> InferM NominalType
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalType
            { ntName :: Name
ntName = Located Name -> Name
forall a. Located a -> a
thing (PrimType Name -> Located Name
forall name. PrimType name -> Located name
P.primTName PrimType Name
p)
            , ntParams :: [TParam]
ntParams = [TParam]
as'
            , ntKind :: Kind
ntKind = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
finK [Kind]
others
            , ntFixity :: Maybe Fixity
ntFixity = PrimType Name -> Maybe Fixity
forall name. PrimType name -> Maybe Fixity
P.primTFixity PrimType Name
p
            , ntConstraints :: [Prop]
ntConstraints = [Prop]
cs'
            , ntDoc :: Maybe Text
ntDoc = Maybe Text
mbD
            , ntDef :: NominalTypeDef
ntDef = NominalTypeDef
Abstract
            }
  where
  splitK :: Kind -> ([Kind], Kind)
splitK Kind
k =
    case Kind
k of
      Kind
k1 :-> Kind
k2 -> (Kind
k1Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
:[Kind]
ks,Kind
r)
        where ([Kind]
ks,Kind
r) = Kind -> ([Kind], Kind)
splitK Kind
k2
      Kind
_ -> ([], Kind
k)


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 = tRebuild 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 NominalType))
-> (NominalType -> KindM Prop) -> KindM Prop -> KindM Prop
forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe NominalType)
kLookupNominal    NominalType -> KindM Prop
checkNominalTypeUse (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
$
  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

  checkNominalTypeUse :: NominalType -> KindM Prop
checkNominalTypeUse NominalType
nt
    | NominalTypeDef
Abstract <- NominalType -> NominalTypeDef
ntDef NominalType
nt =
      do ([Prop]
ts1,Kind
k1) <- [Type Name] -> Kind -> KindM ([Prop], Kind)
appTy [Type Name]
ts (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt)
         let as :: [TParam]
as = NominalType -> [TParam]
ntParams NominalType
nt
             ps :: [Prop]
ps = NominalType -> [Prop]
ntConstraints NominalType
nt
         case [TParam]
as of
           [] -> () -> KindM ()
forall a. a -> KindM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
           [TParam]
_ -> 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 (NominalType -> Name
ntName NominalType
nt) (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 (NominalType -> Name
ntName NominalType
nt)) (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)
         let ty :: Prop
ty =
               -- We must uphold the invariant that built-in abstract types
               -- are represented with TCon. User-defined abstract types use
               -- TNominal instead.
               case Name -> Maybe TCon
builtInType (NominalType -> Name
ntName NominalType
nt) of
                 Just TCon
tc -> TCon -> [Prop] -> Prop
TCon TCon
tc [Prop]
ts1
                 Maybe TCon
Nothing -> NominalType -> [Prop] -> Prop
TNominal NominalType
nt [Prop]
ts1
         Prop -> Maybe Kind -> Kind -> KindM Prop
checkKind Prop
ty Maybe Kind
k Kind
k1

    | Bool
otherwise =
    do ([Prop]
ts1,Kind
k1) <- [Type Name] -> Kind -> KindM ([Prop], Kind)
appTy [Type Name]
ts (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt)
       let as :: [TParam]
as = NominalType -> [TParam]
ntParams NominalType
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) (NominalType -> [Prop]
ntConstraints NominalType
nt)
       ConstraintSource -> [Prop] -> KindM ()
kNewGoals (Name -> ConstraintSource
CtPartialTypeFun (NominalType -> Name
ntName NominalType
nt)) [Prop]
ps1
       Prop -> Maybe Kind -> Kind -> KindM Prop
checkKind (NominalType -> [Prop] -> Prop
TNominal NominalType
nt [Prop]
ts2) 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