-- (c) The University of Glasgow 2006-2012

{-# LANGUAGE CPP #-}
module 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 #-} Type      ( typeKind, substKiWith, eqKind )

import TypeRep
import TysPrim
import TyCon
import VarSet
import PrelNames
import Outputable
import Maybes( orElse )
import Util
import 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