Updated documentation; changed "group" to "branched" in type families
[ghc.git] / compiler / types / Kind.lhs
index e129cc6..0082a33 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The University of Glasgow 2006
+% (c) The University of Glasgow 2006-2012
 %
 
 \begin{code}
 
 module Kind (
         -- * Main data type
-        Kind, typeKind,
+        SuperKind, Kind, typeKind,
 
        -- Kinds
-       anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
-        argTypeKind, ubxTupleKind, constraintKind,
+       anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind,
         mkArrowKind, mkArrowKinds,
-        typeNatKind, typeStringKind,
 
         -- Kind constructors...
         anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
-        unliftedTypeKindTyCon, argTypeKindTyCon, ubxTupleKindTyCon,
-        constraintKindTyCon,
+        unliftedTypeKindTyCon, constraintKindTyCon,
 
         -- Super Kinds
-       tySuperKind, tySuperKindTyCon, 
+       superKind, superKindTyCon, 
         
        pprKind, pprParendKind,
 
@@ -36,19 +33,19 @@ module Kind (
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
-        isUbxTupleKind, isArgTypeKind, isConstraintKind,
-        isConstraintOrLiftedKind, isKind,
-        isSuperKind, noHashInKind,
+        isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
+        isKind, isKindVar,
+        isSuperKind, isSuperKindTyCon,
         isLiftedTypeKindCon, isConstraintKindCon,
         isAnyKind, isAnyKindCon,
+        okArrowArgKind, okArrowResultKind,
 
-        isSubArgTypeKind, tcIsSubArgTypeKind, 
-        isSubOpenTypeKind, tcIsSubOpenTypeKind,
-        isSubKind, tcIsSubKind, defaultKind,
-        isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon,
+        isSubOpenTypeKind, 
+        isSubKind, isSubKindCon, 
+        tcIsSubKind, tcIsSubKindCon,
+        defaultKind,
 
         -- ** Functions on variables
-        isKiVar, splitKiTyVars, partitionKiTyVars,
         kiVarsOfKind, kiVarsOfKinds
 
        ) where
@@ -60,38 +57,10 @@ import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
 import TypeRep
 import TysPrim
 import TyCon
-import Var
 import VarSet
 import PrelNames
 import Outputable
-
-import Data.List ( partition )
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-        Predicates over Kinds
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
--------------------
--- Lastly we need a few functions on Kinds
-
-isLiftedTypeKindCon :: TyCon -> Bool
-isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
-
--- This checks that its argument does not contain # or (#).
--- It is used in tcTyVarBndrs.
-noHashInKind :: Kind -> Bool
-noHashInKind (TyVarTy {}) = True
-noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2
-noHashInKind (ForAllTy _ ki) = noHashInKind ki
-noHashInKind (TyConApp kc kis)
-  =  not (kc `hasKey` unliftedTypeKindTyConKey)
-  && not (kc `hasKey` ubxTupleKindTyConKey)
-  && all noHashInKind kis
-noHashInKind _ = panic "noHashInKind"
+import Util
 \end{code}
 
 %************************************************************************
@@ -100,6 +69,30 @@ noHashInKind _ = panic "noHashInKind"
 %*                                                                     *
 %************************************************************************
 
+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.
+
 \begin{code}
 -- | Essentially 'funResultTy' on kinds handling pi-types too
 kindFunResult :: Kind -> KindOrType -> Kind
@@ -136,41 +129,30 @@ synTyConResKind :: TyCon -> Kind
 synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
 
 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
-isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
+isOpenTypeKind, isUnliftedTypeKind,
   isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
 
-isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
-  isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon,
-  isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon,
-  isAnyKindCon :: TyCon -> Bool
+isOpenTypeKindCon, isUnliftedTypeKindCon,
+  isSubOpenTypeKindCon, isConstraintKindCon,
+  isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
+
 
-isAnyKindCon tc     = tyConUnique tc == anyKindTyConKey
+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
 
-isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
-
 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
 isOpenTypeKind _               = False
 
-isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
-
-isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
-isUbxTupleKind _               = False
-
-isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
-
-isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
-isArgTypeKind _               = False
-
-isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
-
 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 isUnliftedTypeKind _               = False
 
-isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
-
 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 isConstraintKind _               = False
 
@@ -178,103 +160,117 @@ isConstraintOrLiftedKind (TyConApp tc _)
   = isConstraintKindCon tc || isLiftedTypeKindCon tc
 isConstraintOrLiftedKind _ = 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 argTypeKind
-isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of OpenTypeKind
-isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
-isSubOpenTypeKind _                = False
+returnsConstraintKind :: Kind -> Bool
+returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
+returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
+returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
+returnsConstraintKind _               = False
 
--- ^ True of any sub-kind of OpenTypeKind
-tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc
-tcIsSubOpenTypeKind _                = False
+--------------------------------------------
+--            Kinding for arrow (->)
+-- Says when a kind is acceptable on lhs or rhs of an arrow
+--     arg -> res
 
-isSubOpenTypeKindCon kc
-  | isSubArgTypeKindCon kc   = True
-  | isUbxTupleKindCon kc     = True
-  | isOpenTypeKindCon kc     = True
+okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
+okArrowArgKindCon kc
+  | isLiftedTypeKindCon   kc = True
+  | isUnliftedTypeKindCon kc = True
+  | isConstraintKindCon   kc = True
   | otherwise                = False
 
-tcIsSubOpenTypeKindCon kc
-  | tcIsSubArgTypeKindCon kc = True
-  | isUbxTupleKindCon kc     = True
-  | isOpenTypeKindCon kc     = True
-  | otherwise                = False
+okArrowResultKindCon = okArrowArgKindCon
 
-isSubArgTypeKindCon kc
-  | isUnliftedTypeKindCon kc = True
-  | isLiftedTypeKindCon kc   = True
-  | isArgTypeKindCon kc      = True
-  | isConstraintKindCon kc   = True
-  | otherwise                = False
+okArrowArgKind, okArrowResultKind :: Kind -> Bool
+okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
+okArrowArgKind    _                = False
 
-tcIsSubArgTypeKindCon kc
-  | isConstraintKindCon kc   = False
-  | otherwise                = isSubArgTypeKindCon kc
+okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
+okArrowResultKind _                = False
 
-isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of ArgTypeKind 
-isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
-isSubArgTypeKind _                = 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
 
-tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc
-tcIsSubArgTypeKind _                = False
+isSubOpenTypeKind :: Kind -> Bool
+-- ^ True of any sub-kind of OpenTypeKind
+isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
+isSubOpenTypeKind _                = False
 
--- | Is this a super-kind (i.e. a type-of-kinds)?
-isSuperKind :: Type -> Bool
-isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
-isSuperKind _                   = False
+isSubOpenTypeKindCon kc
+  =  isOpenTypeKindCon   kc
+  || isUnliftedTypeKindCon kc
+  || isLiftedTypeKindCon   kc  
+  || isConstraintKindCon kc   -- 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, tcIsSubKind :: Kind -> Kind -> Bool
-isSubKind   = isSubKind' False
-tcIsSubKind = isSubKind' True
-
--- The first argument denotes whether we are in the type-checking phase or not
-isSubKind' :: Bool -> Kind -> Kind -> Bool
+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
 
-isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2)
-  = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2)
-
-isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
-  | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
+-- 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
+  = eqKind k1 k2
 
-  | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
-    -- handles BOX
-    = WARN( not (isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
-                  && null k1s && null k2s), 
-             ppr kc1 <+> ppr kc2 )
-      kc1 == kc2
+  | otherwise -- handles usual kinds (*, #, (#), etc.)
+  = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
+    kc1 `isSubKindCon` kc2
 
-  | otherwise = -- handles usual kinds (*, #, (#), etc.)
-                ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
-                if duringTc then kc1 `tcIsSubKindCon` kc2
-                else kc1 `isSubKindCon` kc2
-
-isSubKind' _duringTc k1 k2 = eqKind k1 k2
+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
-  | isSubArgTypeKindCon  kc1  && isArgTypeKindCon  kc2     = True
-  | isSubOpenTypeKindCon kc1  && isOpenTypeKindCon kc2     = True
-  | otherwise                                              = False
+  | 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
-  | kc1 == kc2                                         = True
-  | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False
-  | otherwise                                          = isSubKindCon kc1 kc2
+  | isConstraintKindCon kc1 = isConstraintKindCon kc2
+  | isConstraintKindCon kc2 = isConstraintKindCon kc1
+  | otherwise               = isSubKindCon kc1 kc2
 
+-------------------------
 defaultKind :: Kind -> Kind
 -- ^ Used when generalising: default OpenKind and ArgKind to *.
 -- See "Type#kind_subtyping" for more information on what that means
@@ -291,21 +287,11 @@ defaultKind :: Kind -> Kind
 -- 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.
-defaultKind k
-  | tcIsSubOpenTypeKind k = liftedTypeKind
-  | otherwise             = k
-
-splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
--- Precondition: kind variables should precede type variables
--- Postcondition: appending the two result lists gives the input!
-splitKiTyVars = span (isSuperKind . tyVarKind)
-
-partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
-partitionKiTyVars = partition (isSuperKind . tyVarKind)
-
--- Checks if this "type or kind" variable is a kind variable
-isKiVar :: TyVar -> Bool
-isKiVar v = isSuperKind (varType v)
+--
+-- The test is really whether the kind is strictly above '*'
+defaultKind (TyConApp kc _args)
+  | isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
+defaultKind k = k
 
 -- Returns the free kind variables in a kind
 kiVarsOfKind :: Kind -> VarSet