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

{-# LANGUAGE CPP #-}
module Kind (
        -- * Main data type
        Kind,

        -- ** Predicates on Kinds
        isLiftedTypeKind, isUnliftedTypeKind,
        isConstraintKindCon,

        classifiesTypeWithValues,
        isKindLevPoly
       ) where

#include "HsVersions.h"

import GhcPrelude

import {-# SOURCE #-} Type    ( coreView )

import TyCoRep
import TyCon
import PrelNames

import Outputable
import Util
import Data.Maybe( isJust )

{-
************************************************************************
*                                                                      *
        Functions over Kinds
*                                                                      *
************************************************************************

Note [Kind Constraint and kind Type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 Type. 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
    C a ~ (a -> a)
so on the left we have Constraint, and on the right we have Type.
See Trac #7451.

Bottom line: although 'Type' and 'Constraint' are distinct TyCons, with
distinct uniques, they are treated as equal at all times except
during type inference.
-}

isConstraintKindCon :: TyCon -> Bool
isConstraintKindCon :: TyCon -> Bool
isConstraintKindCon tc :: TyCon
tc = TyCon -> Unique
tyConUnique TyCon
tc Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
constraintKindTyConKey

-- | Tests whether the given kind (which should look like @TYPE x@)
-- is something other than a constructor tree (that is, constructors at every node).
-- E.g.  True of   TYPE k, TYPE (F Int)
--       False of  TYPE 'LiftedRep
isKindLevPoly :: Kind -> Bool
isKindLevPoly :: Kind -> Bool
isKindLevPoly k :: Kind
k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
                    -- the isLiftedTypeKind check is necessary b/c of Constraint
                  Kind -> Bool
go Kind
k
  where
    go :: Kind -> Bool
go ty :: Kind
ty | Just ty' :: Kind
ty' <- Kind -> Maybe Kind
coreView Kind
ty = Kind -> Bool
go Kind
ty'
    go TyVarTy{}         = Bool
True
    go AppTy{}           = Bool
True  -- it can't be a TyConApp
    go (TyConApp tc :: TyCon
tc tys :: [Kind]
tys) = TyCon -> Bool
isFamilyTyCon TyCon
tc Bool -> Bool -> Bool
|| (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
go [Kind]
tys
    go ForAllTy{}        = Bool
True
    go (FunTy t1 :: Kind
t1 t2 :: Kind
t2)     = Kind -> Bool
go Kind
t1 Bool -> Bool -> Bool
|| Kind -> Bool
go Kind
t2
    go LitTy{}           = Bool
False
    go CastTy{}          = Bool
True
    go CoercionTy{}      = Bool
True

    _is_type :: Bool
_is_type = Kind -> Bool
classifiesTypeWithValues Kind
k

-----------------------------------------
--              Subkinding
-- The tc variants are used during type-checking, where ConstraintKind
-- is distinct from all other kinds
-- After type-checking (in core), Constraint and liftedTypeKind are
-- indistinguishable

-- | Does this classify a type allowed to have values? Responds True to things
-- like *, #, TYPE Lifted, TYPE v, Constraint.
classifiesTypeWithValues :: Kind -> Bool
-- ^ True of any sub-kind of OpenTypeKind
classifiesTypeWithValues :: Kind -> Bool
classifiesTypeWithValues k :: Kind
k = Maybe Kind -> Bool
forall a. Maybe a -> Bool
isJust (HasDebugCallStack => Kind -> Maybe Kind
Kind -> Maybe Kind
kindRep_maybe Kind
k)