-- |
-- 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.ModuleSystem.Name(nameLoc)
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.Error
import           Cryptol.TypeCheck.Subst(listSubst,apSubst,isEmptySubst)
import           Cryptol.TypeCheck.Monad hiding (withTParams)
import           Cryptol.TypeCheck.SimpType(tRebuild)
import           Cryptol.TypeCheck.SimpleSolver(simplify)
import           Cryptol.TypeCheck.Solve ( buildSolverCtxt
                                         , quickSolver
                                         , simplifyAllConstraints
                                         )
import           Cryptol.Utils.Panic (panic)
import           Cryptol.Utils.PP(pp,commaSep)
import           Cryptol.Utils.RecordMap

import           Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import           Data.Foldable(foldlM)
import           Data.List(sortBy,groupBy)
import           Data.Maybe(fromMaybe,isJust)
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 declaration.
-- We check that it has kind either * or #.
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)
      mp :: ModTParam
mp = 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 }
    case Kind
k of
      Kind
KNum -> ModTParam -> InferM ModTParam
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModTParam
mp
      Kind
KType -> ModTParam -> InferM ModTParam
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModTParam
mp
      Kind
_ ->
        do
          let mp' :: ModTParam
mp' = ModTParam
mp { mtpKind = someKind k }
          Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Name -> Range
nameLoc Name
n)
            (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$ Error -> InferM ()
recordError (TParam -> Kind -> [Kind] -> Error
BadParameterKind (ModTParam -> TParam
mtpParam ModTParam
mp') Kind
k [Kind
KNum,Kind
KType])
          ModTParam -> InferM ModTParam
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModTParam
mp'
  where
  -- When we find a malformed kind, we report an error, and correct the kind
  -- according to this function, as the rest of the code expects one of
  -- these kinds.
  someKind :: Kind -> Kind
someKind Kind
e =
    case Kind
e of
      Kind
_ :-> Kind
x -> Kind -> Kind
someKind Kind
x
      Kind
KNum  -> Kind
KNum
      Kind
KType -> Kind
KType
      Kind
KProp -> Kind
KType

-- | 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 [Located Name]
derivs) Maybe Text
mbDoc =
  do (([TParam]
as1,RecordMap Ident Prop
fs1),[Goal]
bodyGs) <- 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

     let name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
         constraints :: [Prop]
constraints = (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
bodyGs
     Map PC [Prop]
derivConds <-
       Name
-> (String, [PC])
-> [Located Name]
-> [Prop]
-> [(Prop, DerivingConstraintSource)]
-> InferM (Map PC [Prop])
checkDeriving Name
name (String, [PC])
newtypeDerivable [Located Name]
derivs [Prop]
constraints
         [(RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
fs1, DerivingConstraintSource
NewtypeUnderlyingRecord)]

     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 = [Prop]
constraints
                    , ntDef :: NominalTypeDef
ntDef = StructCon -> NominalTypeDef
Struct
                                StructCon { ntConName :: Name
ntConName = Name
con, ntFields :: RecordMap Ident Prop
ntFields = RecordMap Ident Prop
fs1 }
                    , ntDeriving :: Map PC [Prop]
ntDeriving = Map PC [Prop]
derivConds
                    , ntFixity :: Maybe Fixity
ntFixity = Maybe Fixity
forall a. Maybe a
Nothing
                    , ntDoc :: Maybe Text
ntDoc = Maybe Text
mbDoc
                    }

-- | A description of newtype declarations, and the supported classes for
-- deriving on newtypes.
newtypeDerivable :: (String, [PC])
newtypeDerivable :: (String, [PC])
newtypeDerivable =
  ( String
"newtype"
  , [PC
PEq, PC
PCmp, PC
PSignedCmp, PC
PZero, PC
PLogic, PC
PRing]
  )

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

     let name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing Located Name
x
         constraints :: [Prop]
constraints = (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
gs
     Map PC [Prop]
derivConds <-
       Name
-> (String, [PC])
-> [Located Name]
-> [Prop]
-> [(Prop, DerivingConstraintSource)]
-> InferM (Map PC [Prop])
checkDeriving Name
name (String, [PC])
enumDerivable (EnumDecl Name -> [Located Name]
forall name. EnumDecl name -> [Located name]
P.eDeriving EnumDecl Name
ed) [Prop]
constraints ([(Prop, DerivingConstraintSource)] -> InferM (Map PC [Prop]))
-> [(Prop, DerivingConstraintSource)] -> InferM (Map PC [Prop])
forall a b. (a -> b) -> a -> b
$
         (EnumCon -> [(Prop, DerivingConstraintSource)])
-> [EnumCon] -> [(Prop, DerivingConstraintSource)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
           (\EnumCon
con -> (Prop -> Int -> (Prop, DerivingConstraintSource))
-> [Prop] -> [Int] -> [(Prop, DerivingConstraintSource)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Prop
t Int
i -> (Prop
t, Name -> Int -> Prop -> DerivingConstraintSource
EnumCtorField (EnumCon -> Name
ecName EnumCon
con) Int
i Prop
t))
                            (EnumCon -> [Prop]
ecFields EnumCon
con)
                            [Int
0..])
           [EnumCon]
cons1

     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 = [Prop]
constraints
                  , ntDef :: NominalTypeDef
ntDef = [EnumCon] -> NominalTypeDef
Enum [EnumCon]
cons1
                  , ntDeriving :: Map PC [Prop]
ntDeriving = Map PC [Prop]
derivConds
                  , ntFixity :: Maybe Fixity
ntFixity = Maybe Fixity
forall a. Maybe a
Nothing
                  , ntDoc :: Maybe Text
ntDoc = Maybe Text
mbD
                  }

-- | A description of enum declarations, and the supported classes for deriving
-- on enums.
enumDerivable :: (String, [PC])
enumDerivable :: (String, [PC])
enumDerivable =
  ( String
"enum"
  , [PC
PEq, PC
PCmp, PC
PSignedCmp]
  )

-- | Check a deriving clause, returning the derived classes and any conditions
-- that must be satisfied for the instances to hold.
checkDeriving ::
     Name
     -- ^ the type being declared
  -> (String, [PC])
     -- ^ description of the type being declared, and the allowed typeclasses
     -- for deriving on this sort of declaration
  -> [Located Name]
     -- ^ list of names in the @deriving@ clause
  -> [Prop]
     -- ^ constraints generated from the type declaration's body
  -> [(Type, DerivingConstraintSource)]
     -- ^ field types within the type declaration, and where they come from
  -> InferM (Map PC [Prop])
     -- ^ map from derived typeclasses to their conditions
checkDeriving :: Name
-> (String, [PC])
-> [Located Name]
-> [Prop]
-> [(Prop, DerivingConstraintSource)]
-> InferM (Map PC [Prop])
checkDeriving Name
declName (String
declDesc, [PC]
allowed) [Located Name]
derivs [Prop]
constraints [(Prop, DerivingConstraintSource)]
fieldTypes = do
  -- Check that the names in the deriving clause are allowed and contain no
  -- duplicates.
  let addDerivRange :: Map PC Range -> Located Name -> InferM (Map PC Range)
addDerivRange Map PC Range
derivRangeMap Located Name
deriv = do
        let derivName :: Name
derivName = Located Name -> Name
forall a. Located a -> a
thing Located Name
deriv
            derivRange :: Range
derivRange = Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
deriv
        case Name -> Maybe TCon
builtInType Name
derivName of
          Just (PC PC
pc)
            | PC
pc PC -> [PC] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PC]
allowed -> do
              let (Maybe Range
existing, Map PC Range
derivRangeMap') =
                    (PC -> Range -> Range -> Range)
-> PC -> Range -> Map PC Range -> (Maybe Range, Map PC Range)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\PC
_ Range
_ Range
old -> Range
old)
                                            PC
pc
                                            Range
derivRange
                                            Map PC Range
derivRangeMap
              Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Range -> Bool
forall a. Maybe a -> Bool
isJust Maybe Range
existing) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
                Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
derivRange (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
                  Warning -> InferM ()
recordWarning (Warning -> InferM ()) -> Warning -> InferM ()
forall a b. (a -> b) -> a -> b
$ PC -> Warning
DuplicateDeriving PC
pc
              Map PC Range -> InferM (Map PC Range)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map PC Range
derivRangeMap'
          Maybe TCon
_ -> do
            Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
derivRange) (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$
              Name -> String -> [PC] -> Error
ClassNotDerivable Name
derivName String
declDesc [PC]
allowed
            Map PC Range -> InferM (Map PC Range)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map PC Range
derivRangeMap
  Map PC Range
derivRangeMap <- (Map PC Range -> Located Name -> InferM (Map PC Range))
-> Map PC Range -> [Located Name] -> InferM (Map PC Range)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Map PC Range -> Located Name -> InferM (Map PC Range)
addDerivRange Map PC Range
forall a. Monoid a => a
mempty [Located Name]
derivs
  -- We can use the functor constraints and the constraints generated from the
  -- body of the type declaration as assumptions for the solver.
  [Located Prop]
paramConstraints <- InferM [Located Prop]
getParamConstraints
  let ctxt :: Ctxt
ctxt = [Prop] -> Ctxt
buildSolverCtxt ([Prop]
constraints [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing [Located Prop]
paramConstraints)
  -- For each derived class, generate its conditions.
  let generateConds :: PC -> Range -> InferM (Maybe [Prop])
generateConds PC
pc Range
derivRange = do
        -- Ensure superclasses are explicitly derived.
        let missingSuperclasses :: Set PC
missingSuperclasses =
              Set PC -> Set PC -> Set PC
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (PC -> Set PC
typeSuperclassSet PC
pc) (Map PC Range -> Set PC
forall k a. Map k a -> Set k
Map.keysSet Map PC Range
derivRangeMap)
        Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set PC -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set PC
missingSuperclasses) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
          Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
derivRange) (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$
            PC -> [PC] -> Error
DerivingMissingSuperclasses PC
pc (Set PC -> [PC]
forall a. Set a -> [a]
Set.toList Set PC
missingSuperclasses)
        -- All fields in the type declaration must be instances of each class.
        let goals :: [Goal]
goals =
              ((Prop, DerivingConstraintSource) -> Goal)
-> [(Prop, DerivingConstraintSource)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (\(Prop
ty, DerivingConstraintSource
which) ->
                    Goal { goal :: Prop
goal = TCon -> [Prop] -> Prop
TCon (PC -> TCon
PC PC
pc) [Prop
ty]
                         , goalSource :: ConstraintSource
goalSource = Name -> PC -> DerivingConstraintSource -> ConstraintSource
CtDeriving Name
declName PC
pc DerivingConstraintSource
which
                         , goalRange :: Range
goalRange = Range
derivRange
                         })
                  [(Prop, DerivingConstraintSource)]
fieldTypes
        case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
goals of
          Right (Subst
su, [Goal]
conds)
            -- Since we are not doing type inference, su should be empty.
            | Subst -> Bool
isEmptySubst Subst
su ->
              -- conds contains the goals that the solver was unable to solve,
              -- but unable to rule out either (e.g. goals involving a type
              -- parameter, which can only be solved when this nominal type is
              -- actually used). These are the conditions that we want to save
              -- in the 'NominalType', so they can be checked at the use site of
              -- the class methods.
              Maybe [Prop] -> InferM (Maybe [Prop])
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [Prop] -> InferM (Maybe [Prop]))
-> Maybe [Prop] -> InferM (Maybe [Prop])
forall a b. (a -> b) -> a -> b
$ [Prop] -> Maybe [Prop]
forall a. a -> Maybe a
Just ([Prop] -> Maybe [Prop]) -> [Prop] -> Maybe [Prop]
forall a b. (a -> b) -> a -> b
$ (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
conds
            | Bool
otherwise ->
              String -> [String] -> InferM (Maybe [Prop])
forall a. HasCallStack => String -> [String] -> a
panic String
"checkDeriving"
                [ String
"Solver substitution not empty"
                , String
"ctxt: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ctxt -> String
forall a. Show a => a -> String
show Ctxt
ctxt
                , String
"goals: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Goal] -> String
forall a. Show a => a -> String
show [Goal]
goals
                , String
"su: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Subst -> String
forall a. Show a => a -> String
show Subst
su
                , String
"conds: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Goal] -> String
forall a. Show a => a -> String
show [Goal]
conds
                ]
          Left Error
err -> do
            -- If there were unsolvable (impossible) goals, that means some
            -- fields were not instances of this class. Report the error here.
            Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
derivRange) Error
err
            Maybe [Prop] -> InferM (Maybe [Prop])
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Prop]
forall a. Maybe a
Nothing
  (PC -> Range -> InferM (Maybe [Prop]))
-> Map PC Range -> InferM (Map PC [Prop])
forall (f :: * -> *) k a b.
Applicative f =>
(k -> a -> f (Maybe b)) -> Map k a -> f (Map k b)
Map.traverseMaybeWithKey PC -> Range -> InferM (Maybe [Prop])
generateConds Map PC Range
derivRangeMap

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
            , ntDeriving :: Map PC [Prop]
ntDeriving = Map PC [Prop]
forall a. Monoid a => a
mempty
            }
  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 Located Name
x [Type Name]
ts    -> Name -> [Type Name] -> Maybe Kind -> KindM Prop
checkTUser (Located Name -> Name
forall a. Located a -> a
thing Located 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 (Located Name -> [Type Name] -> Type Name
forall n. Located n -> [Type n] -> Type n
P.TUser 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