-- (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 tc = tyConUnique tc == 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 k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
-- the isLiftedTypeKind check is necessary b/c of Constraint
go k
where
go ty | Just ty' <- coreView ty = go ty'
go TyVarTy{} = True
go AppTy{} = True -- it can't be a TyConApp
go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
go ForAllTy{} = True
go (FunTy t1 t2) = go t1 || go t2
go LitTy{} = False
go CastTy{} = True
go CoercionTy{} = True
_is_type = classifiesTypeWithValues 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 k = isJust (kindRep_maybe k)