content: -- (c) The University of Glasgow 2006-2012
  
  {-# LANGUAGE CPP #-}
  module Eta.Types.Kind (
          -- * Main data type
          SuperKind, Kind, typeKind,
  
          -- Kinds
          anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind,
          mkArrowKind, mkArrowKinds,
  
          -- Kind constructors...
          anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
          unliftedTypeKindTyCon, constraintKindTyCon,
  
          -- Super Kinds
          superKind, superKindTyCon,
  
          pprKind, pprParendKind,
  
          -- ** Deconstructing Kinds
          kindAppResult, synTyConResKind,
          splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
  
          -- ** Predicates on Kinds
          isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
          isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
          isKind, isKindVar,
          isSuperKind, isSuperKindTyCon,
          isLiftedTypeKindCon, isConstraintKindCon,
          isAnyKind, isAnyKindCon,
          okArrowArgKind, okArrowResultKind,
  
          isSubOpenTypeKind, isSubOpenTypeKindKey,
          isSubKind, isSubKindCon,
          tcIsSubKind, tcIsSubKindCon,
          defaultKind, defaultKind_maybe,
  
          -- ** Functions on variables
          kiVarsOfKind, kiVarsOfKinds
  
         ) where
  
  #include "HsVersions.h"
  
  import {-# SOURCE #-} Eta.Types.Type      ( typeKind, substKiWith, eqKind )
  
  import Eta.Types.TypeRep
  import Eta.Prelude.TysPrim
  import Eta.Types.TyCon
  import Eta.BasicTypes.VarSet
  import Eta.Prelude.PrelNames
  import Eta.Utils.Outputable
  import Eta.Utils.Maybes( orElse )
  import Eta.Utils.Util
  import Eta.Utils.FastString
  
  {-
  ************************************************************************
  *                                                                      *
          Functions over Kinds
  *                                                                      *
  ************************************************************************
  
  Note [Kind Constraint and kind *]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  The kind Constraint is the kind of classes and other type constraints.
  The special thing about types of kind Constraint is that
   * They are displayed with double arrow:
       f :: Ord a => a -> a
   * They are implicitly instantiated at call sites; so the type inference
     engine inserts an extra argument of type (Ord a) at every call site
     to f.
  
  However, once type inference is over, there is *no* distinction between
  Constraint and *.  Indeed we can have coercions between the two. Consider
     class C a where
       op :: a -> a
  For this single-method class we may generate a newtype, which in turn
  generates an axiom witnessing
      Ord a ~ (a -> a)
  so on the left we have Constraint, and on the right we have *.
  See Trac #7451.
  
  Bottom line: although '*' and 'Constraint' are distinct TyCons, with
  distinct uniques, they are treated as equal at all times except
  during type inference.  Hence cmpTc treats them as equal.
  -}
  
  -- | Essentially 'funResultTy' on kinds handling pi-types too
  kindFunResult :: SDoc -> Kind -> KindOrType -> Kind
  kindFunResult _ (FunTy _ res)     _   = res
  kindFunResult _ (ForAllTy kv res) arg = substKiWith [kv] [arg] res
  #ifdef DEBUG
  kindFunResult doc k _ = pprPanic "kindFunResult" (ppr k $$ doc)
  #else
  -- Without DEBUG, doc becomes an unsed arg, and will be optimised away
  kindFunResult _ _ _ = panic "kindFunResult"
  #endif
  
  kindAppResult :: SDoc -> Kind -> [Type] -> Kind
  kindAppResult _   k []     = k
  kindAppResult doc k (a:as) = kindAppResult doc (kindFunResult doc k a) as
  
  -- | Essentially 'splitFunTys' on kinds
  splitKindFunTys :: Kind -> ([Kind],Kind)
  splitKindFunTys (FunTy a r) = case splitKindFunTys r of
                                (as, k) -> (a:as, k)
  splitKindFunTys k = ([], k)
  
  splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
  splitKindFunTy_maybe (FunTy a r) = Just (a,r)
  splitKindFunTy_maybe _           = Nothing
  
  -- | Essentially 'splitFunTysN' on kinds
  splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
  splitKindFunTysN 0 k           = ([], k)
  splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
                                     (as, k) -> (a:as, k)
  splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
  
  -- | Find the result 'Kind' of a type synonym,
  -- after applying it to its 'arity' number of type variables
  -- Actually this function works fine on data types too,
  -- but they'd always return '*', so we never need to ask
  synTyConResKind :: TyCon -> Kind
  synTyConResKind tycon = kindAppResult (ptext (sLit "synTyConResKind") <+> ppr tycon)
                                        (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
  
  -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
  isOpenTypeKind, isUnliftedTypeKind,
    isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
  
  isOpenTypeKindCon, isUnliftedTypeKindCon,
    isSubOpenTypeKindCon, isConstraintKindCon,
    isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
  
  
  isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
  isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
  isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
  isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
  isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
  isSuperKindTyCon      tc = tyConUnique tc == superKindTyConKey
  
  isAnyKind (TyConApp tc _) = isAnyKindCon tc
  isAnyKind _               = False
  
  isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
  isOpenTypeKind _               = False
  
  isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
  isUnliftedTypeKind _               = False
  
  isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
  isConstraintKind _               = False
  
  isConstraintOrLiftedKind (TyConApp tc _)
    = isConstraintKindCon tc || isLiftedTypeKindCon tc
  isConstraintOrLiftedKind _ = False
  
  returnsConstraintKind :: Kind -> Bool
  returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
  returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
  returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
  returnsConstraintKind _               = False
  
  --------------------------------------------
  --            Kinding for arrow (->)
  -- Says when a kind is acceptable on lhs or rhs of an arrow
  --     arg -> res
  
  okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
  okArrowArgKindCon    = isSubOpenTypeKindCon
  okArrowResultKindCon = isSubOpenTypeKindCon
  
  okArrowArgKind, okArrowResultKind :: Kind -> Bool
  okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
  okArrowArgKind    _                = False
  
  okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
  okArrowResultKind _                = False
  
  -----------------------------------------
  --              Subkinding
  -- The tc variants are used during type-checking, where we don't want the
  -- Constraint kind to be a subkind of anything
  -- After type-checking (in core), Constraint is a subkind of openTypeKind
  
  isSubOpenTypeKind :: Kind -> Bool
  -- ^ True of any sub-kind of OpenTypeKind
  isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
  isSubOpenTypeKind _                = False
  
  isSubOpenTypeKindCon kc = isSubOpenTypeKindKey (tyConUnique kc)
  
  isSubOpenTypeKindKey :: Unique -> Bool
  isSubOpenTypeKindKey uniq
    =  uniq == openTypeKindTyConKey
    || uniq == unliftedTypeKindTyConKey
    || uniq == liftedTypeKindTyConKey
    || uniq == constraintKindTyConKey  -- Needed for error (Num a) "blah"
                                       -- and so that (Ord a -> Eq a) is well-kinded
                                       -- and so that (# Eq a, Ord b #) is well-kinded
                                       -- See Note [Kind Constraint and kind *]
  
  -- | Is this a kind (i.e. a type-of-types)?
  isKind :: Kind -> Bool
  isKind k = isSuperKind (typeKind k)
  
  isSubKind :: Kind -> Kind -> Bool
  -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
  -- Sub-kinding is extremely simple and does not look
  -- under arrrows or type constructors
  
  -- If you edit this function, you may need to update the GHC formalism
  -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
  isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
    | isPromotedTyCon kc1 || isPromotedTyCon kc2
      -- handles promoted kinds (List *, Nat, etc.)
    = eqKind k1 k2
  
    | otherwise -- handles usual kinds (*, #, (#), etc.)
    = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
      kc1 `isSubKindCon` kc2
  
  isSubKind k1 k2 = eqKind k1 k2
  
  isSubKindCon :: TyCon -> TyCon -> Bool
  -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
  
  -- If you edit this function, you may need to update the GHC formalism
  -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
  isSubKindCon kc1 kc2
    | kc1 == kc2              = True
    | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1
    | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
    | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
      -- See Note [Kind Constraint and kind *]
    | otherwise               = False
  
  -------------------------
  -- Hack alert: we need a tiny variant for the typechecker
  -- Reason:     f :: Int -> (a~b)
  --             g :: forall (c::Constraint). Int -> c
  --             h :: Int => Int
  -- We want to reject these, even though Constraint is
  -- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
  -- *after* the typechecker
  --   a) So that (Ord a -> Eq a) is a legal type
  --   b) So that the simplifer can generate (error (Eq a) "urk")
  -- Moreover, after the type checker, Constraint and *
  -- are identical; see Note [Kind Constraint and kind *]
  --
  -- Easiest way to reject is simply to make Constraint a compliete
  -- below OpenTypeKind when type checking
  
  tcIsSubKind :: Kind -> Kind -> Bool
  tcIsSubKind k1 k2
    | isConstraintKind k1 = isConstraintKind k2
    | isConstraintKind k2 = isConstraintKind k1
    | otherwise           = isSubKind k1 k2
  
  tcIsSubKindCon :: TyCon -> TyCon -> Bool
  tcIsSubKindCon kc1 kc2
    | isConstraintKindCon kc1 = isConstraintKindCon kc2
    | isConstraintKindCon kc2 = isConstraintKindCon kc1
    | otherwise               = isSubKindCon kc1 kc2
  
  -------------------------
  defaultKind       :: Kind -> Kind
  defaultKind_maybe :: Kind -> Maybe Kind
  -- ^ Used when generalising: default OpenKind and ArgKind to *.
  -- See "Type#kind_subtyping" for more information on what that means
  
  -- When we generalise, we make generic type variables whose kind is
  -- simple (* or *->* etc).  So generic type variables (other than
  -- built-in constants like 'error') always have simple kinds.  This is important;
  -- consider
  --      f x = True
  -- We want f to get type
  --      f :: forall (a::*). a -> Bool
  -- Not
  --      f :: forall (a::ArgKind). a -> Bool
  -- because that would allow a call like (f 3#) as well as (f True),
  -- and the calling conventions differ.
  -- This defaulting is done in TcMType.zonkTcTyVarBndr.
  --
  -- The test is really whether the kind is strictly above '*'
  defaultKind_maybe (TyConApp kc _args)
    | isOpenTypeKindCon kc = ASSERT( null _args ) Just liftedTypeKind
  defaultKind_maybe _      = Nothing
  
  defaultKind k = defaultKind_maybe k `orElse` k
  
  -- Returns the free kind variables in a kind
  kiVarsOfKind :: Kind -> VarSet
  kiVarsOfKind = tyVarsOfType
  
  kiVarsOfKinds :: [Kind] -> VarSet
  kiVarsOfKinds = tyVarsOfTypes
  