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

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

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

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

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

  where
  rng :: InferM a -> InferM a
rng = case Maybe Range
mb of
          Maybe Range
Nothing -> forall a. a -> a
id
          Just Range
r  -> 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) <- forall a. InferM a -> InferM (a, [Goal])
collectGoals (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Located (Prop Name) -> InferM Prop
check [Located (Prop Name)]
props)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure [Prop]
newPs
  where
  check :: Located (Prop Name) -> InferM Prop
check Located (Prop Name)
lp =
    forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located (Prop Name)
lp)
    do let p :: Prop Name
p = forall a. Located a -> a
thing Located (Prop Name)
lp
       ([TParam]
_,Prop
ps) <- 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PC
PEqual,PC
PNeq,PC
PGeq,PC
PFin,PC
PTrue] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
         Prop
_ -> Error -> InferM ()
recordError (Prop -> Error
InvalidConstraintGuard Prop
ps)
       forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
ps



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


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

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

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

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

checkType :: P.Type Name -> Maybe Kind -> InferM Type
checkType :: Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
t Maybe Kind
k =
  do ([TParam]
_, Prop
t1) <- forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
AllowWildCards Name -> TPFlavor
schemaParam [] forall a b. (a -> b) -> a -> b
$ Type Name -> Maybe Kind -> KindM Prop
doCheckType Type Name
t Maybe Kind
k
     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) <- forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
NoWildCards Name -> TPFlavor
schemaParam [] (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Located (Prop Name) -> KindM (Located Prop)
checkL [Located (Prop Name)]
ps)
     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 (forall a. Located a -> a
thing Located (Prop Name)
x)
                forall (m :: * -> *) a. Monad m => a -> m a
return Located (Prop Name)
x { thing :: Prop
thing = Prop -> Prop
tRebuild Prop
p }


{- | Check something with type parameters.

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

Here is an example of how this may show up:

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

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

> f `{n = 3}

There are two reasons for this choice:

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

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

withTParams :: AllowWildCards    {- ^ Do we allow wild cards -} ->
              (Name -> TPFlavor) {- ^ What sort of params are these? -} ->
              [P.TParam Name]    {- ^ The params -} ->
              KindM a            {- ^ do this using the params -} ->
              InferM ([TParam], a)
withTParams :: forall a.
AllowWildCards
-> (Name -> TPFlavor)
-> [TParam Name]
-> KindM a
-> InferM ([TParam], a)
withTParams AllowWildCards
allowWildCards Name -> TPFlavor
flav [TParam Name]
xs KindM a
m
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[TParam Name]]
duplicates) = forall a. HasCallStack => String -> [String] -> a
panic String
"withTParams" forall a b. (a -> b) -> a -> b
$ String
"Repeated parameters"
                                                forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map 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) <- forall a.
AllowWildCards
-> [(Name, Maybe Kind, TParam)]
-> KindM a
-> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
runKindM AllowWildCards
allowWildCards (forall {n} {c}. [TParam n] -> [c] -> [(n, Maybe Kind, c)]
zip' [TParam Name]
xs [TParam]
as) KindM a
m
            [TParam]
as <- 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
            forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam]
as,a
a,[(ConstraintSource, [Prop])]
ctrs)
     forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ConstraintSource -> [Prop] -> InferM ()
newGoals) [(ConstraintSource, [Prop])]
ctrs
     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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall n. TParam n -> n
P.tpName TParam Name
tp) Map Name Kind
vs of
      Just Kind
k  -> 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)
                    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 = 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) = (forall n. TParam n -> n
P.tpName TParam n
a, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Kind -> Kind
cvtK (forall n. TParam n -> Maybe Kind
P.tpKind TParam n
a), c
t) 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]
_) <- forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall n. TParam n -> n
P.tpName)
                                      forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 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 (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 =
  forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe LkpTyVar)
kLookupTyVar      LkpTyVar -> KindM Prop
checkBoundVarUse forall a b. (a -> b) -> a -> b
$
  forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe TySyn)
kLookupTSyn       TySyn -> KindM Prop
checkTySynUse forall a b. (a -> b) -> a -> b
$
  forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe Newtype)
kLookupNewtype    Newtype -> KindM Prop
checkNewTypeUse forall a b. (a -> b) -> a -> b
$
  forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe ModTParam)
kLookupParamType  ModTParam -> KindM Prop
checkModuleParamUse forall a b. (a -> b) -> a -> b
$
  forall a.
(Name -> KindM (Maybe a))
-> (a -> KindM Prop) -> KindM Prop -> KindM Prop
mcase Name -> KindM (Maybe AbstractType)
kLookupAbstractType AbstractType -> KindM Prop
checkAbstractTypeUse 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 (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 = forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
as [Prop]
ts2
       [Prop]
ps1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Prop -> [(TParam, Prop)] -> KindM Prop
`kInstantiateT` [(TParam, Prop)]
su) (TySyn -> [Prop]
tsConstraints TySyn
tysyn)
       ConstraintSource -> [Prop] -> KindM ()
kNewGoals (Name -> ConstraintSource
CtPartialTypeFun (TySyn -> Name
tsName TySyn
tysyn)) [Prop]
ps1
       Prop
t1  <- Prop -> [(TParam, Prop)] -> KindM Prop
kInstantiateT (TySyn -> Prop
tsDef TySyn
tysyn) [(TParam, Prop)]
su
       Prop -> Maybe Kind -> Kind -> KindM Prop
checkKind (Name -> [Prop] -> Prop -> Prop
TUser Name
x [Prop]
ts1 Prop
t1) Maybe Kind
k Kind
k1

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

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

  checkParams :: [TParam] -> [Prop] -> KindM [Prop]
checkParams [TParam]
as [Prop]
ts1
    | Int
paramHave forall a. Eq a => a -> a -> Bool
== Int
paramNeed = forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
ts1
    | Int
paramHave forall a. Ord a => a -> a -> Bool
< Int
paramNeed  =
                   do Error -> KindM ()
kRecordError (Name -> Int -> Error
TooFewTyParams Name
x (Int
paramNeedforall a. Num a => a -> a -> a
-Int
paramHave))
                      let src :: TypeSource
src = TypeSource
TypeErrorPlaceHolder
                      [Prop]
fake <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TypeSource -> Kind -> KindM Prop
kNewType TypeSource
src forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasKind t => t -> Kind
kindOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar)
                                   (forall a. Int -> [a] -> [a]
drop Int
paramHave [TParam]
as)
                      forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop]
ts1 forall a. [a] -> [a] -> [a]
++ [Prop]
fake)
    | Bool
otherwise = do Error -> KindM ()
kRecordError (Name -> Int -> Error
TooManyTySynParams Name
x (Int
paramHaveforall a. Num a => a -> a -> a
-Int
paramNeed))
                     forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Int -> [a] -> [a]
take Int
paramNeed [Prop]
ts1)
    where paramHave :: Int
paramHave = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
ts1
          paramNeed :: Int
paramNeed = 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 (forall t. HasKind t => t -> Kind
kindOf TVar
ty)
       case Maybe Kind
k of
         Just Kind
ks
           | Kind
ks forall a. Eq a => a -> a -> Bool
/= Kind
k1 -> Error -> KindM ()
kRecordError (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch forall a. Maybe a
Nothing Kind
ks Kind
k1)
         Maybe Kind
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

  checkBoundVarUse :: LkpTyVar -> KindM Prop
checkBoundVarUse LkpTyVar
v =
    do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type Name]
ts) 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 -> 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 (forall t. HasKind t => t -> Kind
kindOf TParam
t)

  checkScopedVarUse :: KindM Prop
checkScopedVarUse =
    do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type Name]
ts) (Error -> KindM ()
kRecordError Error
TyVarWithParams)
       Name -> Kind -> KindM Prop
kExistTVar Name
x forall a b. (a -> b) -> a -> b
$ 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 = 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 (forall a. a -> Maybe a
Just Kind
k1)
     ([Prop]
ts1,Kind
k) <- [Type Name] -> Kind -> KindM ([Prop], Kind)
appTy [Type Name]
ts Kind
k2
     forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
t1 forall a. a -> [a] -> [a]
: [Prop]
ts1, Kind
k)

appTy [Type Name]
ts Kind
k1 =
  do Error -> KindM ()
kRecordError (Int -> Kind -> Error
TooManyTypeParams (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type Name]
ts) Kind
k1)
     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 -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k1
                      Maybe Kind
Nothing -> do Warning -> KindM ()
kRecordWarning (Kind -> Warning
DefaultingWildType Kind
P.KNum)
                                    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 forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ 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 (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap 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 -> forall a. Range -> KindM a -> KindM a
kInRange Range
r1 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Kind
mb) of
                   (Just Kind
a, Just Kind
b) ->
                      do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
a forall a. Eq a => a -> a -> Bool
== Kind
b)
                           (Error -> KindM ()
kRecordError (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch forall a. Maybe a
Nothing Kind
a Kind
b))
                         forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just Kind
b)
                   (Maybe Kind
a,Maybe Kind
b) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 (forall n. n -> [Type n] -> Type n
P.TUser (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) = forall a. Range -> KindM a -> KindM a
kInRange Range
rng forall a b. (a -> b) -> a -> b
$ Type Name -> Maybe Kind -> KindM Prop
doCheckType Type Name
v (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 (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 forall a. Eq a => a -> a -> Bool
/= Kind
k2    = do Error -> KindM ()
kRecordError (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch forall a. Maybe a
Nothing Kind
k1 Kind
k2)
                     TypeSource -> Kind -> KindM Prop
kNewType TypeSource
TypeErrorPlaceHolder Kind
k1
checkKind Prop
t Maybe Kind
_ Kind
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t