Kind.hs 4.91 KB
Newer Older
1
-- (c) The University of Glasgow 2006-2012
2

3
{-# LANGUAGE CPP #-}
4 5
module Kind (
        -- * Main data type
6
        Kind, typeKind,
7 8

        -- ** Predicates on Kinds
9 10 11 12
        isLiftedTypeKind, isUnliftedTypeKind,
        isConstraintKind,
        returnsTyCon, returnsConstraintKind,
        isConstraintKindCon,
13
        okArrowArgKind, okArrowResultKind,
14

15 16
        classifiesTypeWithValues,
        isStarKind, isStarKindSynonymTyCon,
17
        isRuntimeRepPolymorphic
18 19 20 21
       ) where

#include "HsVersions.h"

22
import {-# SOURCE #-} Type       ( typeKind, coreViewOneStarKind )
batterseapower's avatar
batterseapower committed
23

24
import TyCoRep
25
import TyCon
26
import VarSet ( isEmptyVarSet )
27 28
import PrelNames

29 30 31
{-
************************************************************************
*                                                                      *
32
        Functions over Kinds
33 34
*                                                                      *
************************************************************************
35

36 37 38
Note [Kind Constraint and kind *]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The kind Constraint is the kind of classes and other type constraints.
39
The special thing about types of kind Constraint is that
40 41 42 43 44 45
 * 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.

46
However, once type inference is over, there is *no* distinction between
47 48 49
Constraint and *.  Indeed we can have coercions between the two. Consider
   class C a where
     op :: a -> a
50
For this single-method class we may generate a newtype, which in turn
51
generates an axiom witnessing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
52
    C a ~ (a -> a)
53 54 55 56
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
57
distinct uniques, they are treated as equal at all times except
58
during type inference.
59
-}
60

61 62
isConstraintKind :: Kind -> Bool
isConstraintKindCon :: TyCon -> Bool
63

64
isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
65

batterseapower's avatar
batterseapower committed
66 67 68
isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
isConstraintKind _               = False

69 70 71 72
-- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
-- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
returnsTyCon :: Unique -> Type -> Bool
returnsTyCon tc_u (ForAllTy _ ty)  = returnsTyCon tc_u ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
73
returnsTyCon tc_u (FunTy    _ ty)  = returnsTyCon tc_u ty
74 75
returnsTyCon tc_u (TyConApp tc' _) = tc' `hasKey` tc_u
returnsTyCon _  _                  = False
dreixel's avatar
dreixel committed
76

77
returnsConstraintKind :: Kind -> Bool
78 79
returnsConstraintKind = returnsTyCon constraintKindTyConKey

80 81 82 83 84
-- | Tests whether the given type (which should look like "TYPE ...") has any
-- free variables
isRuntimeRepPolymorphic :: Kind -> Bool
isRuntimeRepPolymorphic k
  = not $ isEmptyVarSet $ tyCoVarsOfType k
85

86 87 88 89
--------------------------------------------
--            Kinding for arrow (->)
-- Says when a kind is acceptable on lhs or rhs of an arrow
--     arg -> res
90 91
--
-- See Note [Levity polymorphism]
92 93

okArrowArgKind, okArrowResultKind :: Kind -> Bool
94
okArrowArgKind    = classifiesTypeWithValues
95
okArrowResultKind = classifiesTypeWithValues
96 97 98

-----------------------------------------
--              Subkinding
99 100 101 102 103 104 105 106
-- 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
dreixel's avatar
dreixel committed
107
-- ^ True of any sub-kind of OpenTypeKind
108 109 110 111 112 113 114
classifiesTypeWithValues t | Just t' <- coreViewOneStarKind t = classifiesTypeWithValues t'
classifiesTypeWithValues (TyConApp tc [_]) = tc `hasKey` tYPETyConKey
classifiesTypeWithValues _ = False

-- | Is this kind equivalent to *?
isStarKind :: Kind -> Bool
isStarKind k | Just k' <- coreViewOneStarKind k = isStarKind k'
115 116 117
isStarKind (TyConApp tc [TyConApp ptr_rep []])
  =  tc      `hasKey` tYPETyConKey
  && ptr_rep `hasKey` ptrRepLiftedDataConKey
118 119 120 121 122 123
isStarKind _ = False
                              -- See Note [Kind Constraint and kind *]

-- | Is the tycon @Constraint@?
isStarKindSynonymTyCon :: TyCon -> Bool
isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151


{- Note [Levity polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is this type legal?
   (a :: TYPE rep) -> Int
   where 'rep :: RuntimeRep'

You might think not, because no lambda can have a
runtime-rep-polymorphic binder.  So no lambda has the
above type.  BUT here's a way it can be useful (taken from
Trac #12708):

  data T rep (a :: TYPE rep)
     = MkT (a -> Int)

  x1 :: T LiftedPtrRep Int
  x1 =  MkT LiftedPtrRep Int  (\x::Int -> 3)

  x2 :: T IntRep INt#
  x2 = MkT IntRep Int# (\x:Int# -> 3)

Note that the lambdas are just fine!

Hence, okArrowArgKind and okArrowResultKind both just
check that the type is of the form (TYPE r) for some
representation type r.
-}