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

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

import qualified Cryptol.Parser.AST as P
import           Cryptol.Parser.AST (Named(..))
import           Cryptol.Parser.Position
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.Error
import           Cryptol.TypeCheck.Monad hiding (withTParams)
import           Cryptol.TypeCheck.SimpType(tRebuild)
import           Cryptol.TypeCheck.SimpleSolver(simplify)
import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)
import           Cryptol.TypeCheck.Subst(listSubst,apSubst)
import           Cryptol.Utils.Panic (panic)
import           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,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,([Type]
ps1,Type
t1)), [Goal]
gs) <-
        InferM ([TParam], ([Type], Type))
-> InferM (([TParam], ([Type], Type)), [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM ([TParam], ([Type], Type))
 -> InferM (([TParam], ([Type], Type)), [Goal]))
-> InferM ([TParam], ([Type], Type))
-> InferM (([TParam], ([Type], Type)), [Goal])
forall a b. (a -> b) -> a -> b
$
        InferM ([TParam], ([Type], Type))
-> InferM ([TParam], ([Type], Type))
forall a. InferM a -> InferM a
rng (InferM ([TParam], ([Type], Type))
 -> InferM ([TParam], ([Type], Type)))
-> InferM ([TParam], ([Type], Type))
-> InferM ([TParam], ([Type], Type))
forall a b. (a -> b) -> a -> b
$ AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM ([Type], Type)
-> InferM ([TParam], ([Type], Type))
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
withWild Name -> TPFlavor
schemaParam [TParam Name]
xs (KindM ([Type], Type) -> InferM ([TParam], ([Type], Type)))
-> KindM ([Type], Type) -> InferM ([TParam], ([Type], Type))
forall a b. (a -> b) -> a -> b
$
        do [Type]
ps1 <- (Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Prop Name -> KindM Type
checkProp [Prop Name]
ps
           Type
t1  <- Type Name -> Maybe Kind -> KindM Type
doCheckType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KType)
           ([Type], Type) -> KindM ([Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
ps1,Type
t1)
     -- XXX: We probably shouldn't do this, as we are changing what the
     -- user is doing.  We do it so that things are in a propal normal form,
     -- but we should probably figure out another time to do this.
     let newPs :: [Type]
newPs = (Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Ctxt -> Type -> Type
simplify Ctxt
forall a. Monoid a => a
mempty)
                                     ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
tRebuild [Type]
ps1
     (Schema, [Goal]) -> InferM (Schema, [Goal])
forall (m :: * -> *) a. Monad m => a -> m a
return ( [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
xs1 [Type]
newPs (Type -> Type
tRebuild Type
t1)
            , [ Goal
g { goal :: Type
goal = Type -> Type
tRebuild (Goal -> Type
goal Goal
g) } | Goal
g <- [Goal]
gs ]
            )

  where
  rng :: InferM a -> InferM a
rng = case Maybe Range
mb of
          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

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


-- | Check a type-synonym declaration.
checkTySyn :: P.TySyn Name -> Maybe 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,Type
t1),[Goal]
gs) <- InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
                    (InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal]))
-> InferM ([TParam], Type) -> InferM (([TParam], Type), [Goal])
forall a b. (a -> b) -> a -> b
$ Range -> InferM ([TParam], Type) -> InferM ([TParam], Type)
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x)
                    (InferM ([TParam], Type) -> InferM ([TParam], Type))
-> InferM ([TParam], Type) -> InferM ([TParam], Type)
forall a b. (a -> b) -> a -> b
$ do ([TParam], Type)
r <- AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM Type
-> InferM ([TParam], Type)
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards Name -> TPFlavor
tySynParam [TParam Name]
as
                                                      (Type Name -> Maybe Kind -> KindM Type
doCheckType Type Name
t Maybe Kind
forall a. Maybe a
Nothing)
                         InferM ()
simplifyAllConstraints
                         ([TParam], Type) -> InferM ([TParam], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam], Type)
r
     TySyn -> InferM TySyn
forall (m :: * -> *) a. Monad m => a -> m a
return TySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe Text -> TySyn
TySyn { tsName :: Name
tsName   = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
                  , tsParams :: [TParam]
tsParams = [TParam]
as1
                  , tsConstraints :: [Type]
tsConstraints = (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
tRebuild (Type -> Type) -> (Goal -> Type) -> Goal -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs
                  , tsDef :: Type
tsDef = Type -> Type
tRebuild Type
t1
                  , tsDoc :: Maybe 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,[Type]
t1),[Goal]
gs) <- InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
                    (InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal]))
-> InferM ([TParam], [Type]) -> InferM (([TParam], [Type]), [Goal])
forall a b. (a -> b) -> a -> b
$ Range -> InferM ([TParam], [Type]) -> InferM ([TParam], [Type])
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x)
                    (InferM ([TParam], [Type]) -> InferM ([TParam], [Type]))
-> InferM ([TParam], [Type]) -> InferM ([TParam], [Type])
forall a b. (a -> b) -> a -> b
$ do ([TParam], [Type])
r <- AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM [Type]
-> InferM ([TParam], [Type])
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards Name -> TPFlavor
propSynParam [TParam Name]
as
                                                      ((Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Prop Name -> KindM Type
checkProp [Prop Name]
ps)
                         InferM ()
simplifyAllConstraints
                         ([TParam], [Type]) -> InferM ([TParam], [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam], [Type])
r
     TySyn -> InferM TySyn
forall (m :: * -> *) a. Monad m => a -> m a
return TySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe Text -> TySyn
TySyn { tsName :: Name
tsName   = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
                  , tsParams :: [TParam]
tsParams = [TParam]
as1
                  , tsConstraints :: [Type]
tsConstraints = (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
tRebuild (Type -> Type) -> (Goal -> Type) -> Goal -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs
                  , tsDef :: Type
tsDef = Type -> Type
tRebuild ([Type] -> Type
pAnd [Type]
t1)
                  , tsDoc :: Maybe 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 [Named (Type Name)]
fs) Maybe Text
mbD =
  do (([TParam]
as1,[(Ident, Type)]
fs1),[Goal]
gs) <- InferM ([TParam], [(Ident, Type)])
-> InferM (([TParam], [(Ident, Type)]), [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM ([TParam], [(Ident, Type)])
 -> InferM (([TParam], [(Ident, Type)]), [Goal]))
-> InferM ([TParam], [(Ident, Type)])
-> InferM (([TParam], [(Ident, Type)]), [Goal])
forall a b. (a -> b) -> a -> b
$
       Range
-> InferM ([TParam], [(Ident, Type)])
-> InferM ([TParam], [(Ident, Type)])
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x) (InferM ([TParam], [(Ident, Type)])
 -> InferM ([TParam], [(Ident, Type)]))
-> InferM ([TParam], [(Ident, Type)])
-> InferM ([TParam], [(Ident, Type)])
forall a b. (a -> b) -> a -> b
$
       do ([TParam], [(Ident, Type)])
r <- AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM [(Ident, Type)]
-> InferM ([TParam], [(Ident, Type)])
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards Name -> TPFlavor
newtypeParam [TParam Name]
as (KindM [(Ident, Type)] -> InferM ([TParam], [(Ident, Type)]))
-> KindM [(Ident, Type)] -> InferM ([TParam], [(Ident, Type)])
forall a b. (a -> b) -> a -> b
$
               [Named (Type Name)]
-> (Named (Type Name) -> KindM (Ident, Type))
-> KindM [(Ident, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Named (Type Name)]
fs ((Named (Type Name) -> KindM (Ident, Type))
 -> KindM [(Ident, Type)])
-> (Named (Type Name) -> KindM (Ident, Type))
-> KindM [(Ident, Type)]
forall a b. (a -> b) -> a -> b
$ \Named (Type Name)
field ->
                 let n :: Located Ident
n = Named (Type Name) -> Located Ident
forall a. Named a -> Located Ident
name Named (Type Name)
field
                 in Range -> KindM (Ident, Type) -> KindM (Ident, Type)
forall a. Range -> KindM a -> KindM a
kInRange (Located Ident -> Range
forall a. Located a -> Range
srcRange Located Ident
n) (KindM (Ident, Type) -> KindM (Ident, Type))
-> KindM (Ident, Type) -> KindM (Ident, Type)
forall a b. (a -> b) -> a -> b
$
                    do Type
t1 <- Type Name -> Maybe Kind -> KindM Type
doCheckType (Named (Type Name) -> Type Name
forall a. Named a -> a
value Named (Type Name)
field) (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KType)
                       (Ident, Type) -> KindM (Ident, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
n, Type
t1)
          InferM ()
simplifyAllConstraints
          ([TParam], [(Ident, Type)]) -> InferM ([TParam], [(Ident, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam], [(Ident, Type)])
r

     Newtype -> InferM Newtype
forall (m :: * -> *) a. Monad m => a -> m a
return Newtype :: Name
-> [TParam] -> [Type] -> [(Ident, Type)] -> Maybe Text -> Newtype
Newtype { ntName :: Name
ntName   = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
                    , ntParams :: [TParam]
ntParams = [TParam]
as1
                    , ntConstraints :: [Type]
ntConstraints = (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs
                    , ntFields :: [(Ident, Type)]
ntFields = [(Ident, Type)]
fs1
                    , ntDoc :: Maybe 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',[Type]
cs') <- AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM [Type]
-> InferM ([TParam], [Type])
forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards (Maybe Name -> TPFlavor
TPOther (Maybe Name -> TPFlavor)
-> (Name -> Maybe Name) -> Name -> TPFlavor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Maybe Name
forall a. a -> Maybe a
Just) [TParam Name]
as (KindM [Type] -> InferM ([TParam], [Type]))
-> KindM [Type] -> InferM ([TParam], [Type])
forall a b. (a -> b) -> a -> b
$
                    (Prop Name -> KindM Type) -> [Prop Name] -> KindM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Prop Name -> KindM Type
checkProp [Prop Name]
cs
     AbstractType -> InferM AbstractType
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbstractType :: Name
-> Kind
-> ([TParam], [Type])
-> Maybe Fixity
-> Maybe Text
-> AbstractType
AbstractType { atName :: Name
atName = Located Name -> Name
forall a. Located a -> a
thing (PrimType Name -> Located Name
forall name. PrimType name -> Located name
P.primTName PrimType Name
p)
                       , atKind :: Kind
atKind = Kind -> Kind
cvtK (Located Kind -> Kind
forall a. Located a -> a
thing (PrimType Name -> Located Kind
forall name. PrimType name -> Located Kind
P.primTKind PrimType Name
p))
                       , atFixitiy :: Maybe Fixity
atFixitiy = PrimType Name -> Maybe Fixity
forall name. PrimType name -> Maybe Fixity
P.primTFixity PrimType Name
p
                       , atCtrs :: ([TParam], [Type])
atCtrs = ([TParam]
as',[Type]
cs')
                       , atDoc :: Maybe Text
atDoc = Maybe Text
mbD
                       }

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

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


{- | Check something with type parameters.

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

Here is an example of how this may show up:

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

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

> f `{n = 3}

There are two reasons for this choice:

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

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

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

  where
  getKind :: Map Name Kind -> TParam Name -> InferM Kind
getKind 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 (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 (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 (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 Type
tcon TCon
tc [Type Name]
ts0 Maybe Kind
k =
  do ([Type]
ts1,Kind
k1) <- [Type Name] -> Kind -> KindM ([Type], Kind)
appTy [Type Name]
ts0 (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
tc)
     Type -> Maybe Kind -> Kind -> KindM Type
checkKind (TCon -> [Type] -> Type
TCon TCon
tc [Type]
ts1) Maybe Kind
k Kind
k1


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

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

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

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



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

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

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

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

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

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

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

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

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


-- | Validate a parsed type.
doCheckType :: P.Type Name  -- ^ Type that needs to be checked
          -> Maybe Kind     -- ^ Expected kind (if any)
          -> KindM Type     -- ^ Checked type
doCheckType :: Type Name -> Maybe Kind -> KindM Type
doCheckType 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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Kind
KNum
         TypeSource -> Kind -> KindM Type
kNewType TypeSource
TypeWildCard Kind
theKind

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

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

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

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

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

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

    P.TTyApp [Named (Type Name)]
_fs    -> String -> [String] -> KindM Type
forall a. HasCallStack => String -> [String] -> a
panic String
"doCheckType"
                         [String
"TTyApp found when kind checking, but it should have been eliminated already"]

  where
  checkF :: p -> (Range, Type Name) -> KindM Type
checkF p
_nm (Range
rng,Type Name
v) = Range -> KindM Type -> KindM Type
forall a. Range -> KindM a -> KindM a
kInRange Range
rng (KindM Type -> KindM Type) -> KindM Type -> KindM Type
forall a b. (a -> b) -> a -> b
$ Type Name -> Maybe Kind -> KindM Type
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 Type       -- ^ Checked representation
checkProp :: Prop Name -> KindM Type
checkProp (P.CType Type Name
t) = Type Name -> Maybe Kind -> KindM Type
doCheckType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KProp)


-- | Check that a type has the expected kind.
checkKind :: Type         -- ^ Kind-checked type
          -> Maybe Kind   -- ^ Expected kind (if any)
          -> Kind         -- ^ Inferred kind
          -> KindM Type   -- ^ A type consistent with expectations.
checkKind :: Type -> Maybe Kind -> Kind -> KindM Type
checkKind Type
_ (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 Type
kNewType TypeSource
TypeErrorPlaceHolder Kind
k1
checkKind Type
t Maybe Kind
_ Kind
_ = Type -> KindM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t