Updated documentation; changed "group" to "branched" in type families
[ghc.git] / compiler / types / Kind.lhs
index c0364fa..0082a33 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The University of Glasgow 2006
+% (c) The University of Glasgow 2006-2012
 %
 
 \begin{code}
@@ -15,15 +15,12 @@ module Kind (
         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
        superKind, superKindTyCon, 
@@ -36,14 +33,14 @@ module Kind (
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
-        isUbxTupleKind, isArgTypeKind, isConstraintKind,
-        isConstraintOrLiftedKind, isKind, isKindVar,
+        isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
+        isKind, isKindVar,
         isSuperKind, isSuperKindTyCon,
         isLiftedTypeKindCon, isConstraintKindCon,
         isAnyKind, isAnyKindCon,
         okArrowArgKind, okArrowResultKind,
 
-        isSubArgTypeKind, isSubOpenTypeKind, 
+        isSubOpenTypeKind, 
         isSubKind, isSubKindCon, 
         tcIsSubKind, tcIsSubKindCon,
         defaultKind,
@@ -63,6 +60,7 @@ import TyCon
 import VarSet
 import PrelNames
 import Outputable
+import Util
 \end{code}
 
 %************************************************************************
@@ -71,6 +69,30 @@ import Outputable
 %*                                                                     *
 %************************************************************************
 
+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
@@ -107,22 +129,20 @@ 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, 
+isOpenTypeKindCon, isUnliftedTypeKindCon,
   isSubOpenTypeKindCon, isConstraintKindCon,
-  isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool
+  isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
 
 
 isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
 isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
 isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
-isUbxTupleKindCon     tc = tyConUnique tc == ubxTupleKindTyConKey
-isArgTypeKindCon      tc = tyConUnique tc == argTypeKindTyConKey
 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
 isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
+isSuperKindTyCon      tc = tyConUnique tc == superKindTyConKey
 
 isAnyKind (TyConApp tc _) = isAnyKindCon tc
 isAnyKind _               = False
@@ -130,12 +150,6 @@ isAnyKind _               = False
 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
 isOpenTypeKind _               = False
 
-isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
-isUbxTupleKind _               = False
-
-isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
-isArgTypeKind _               = False
-
 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 isUnliftedTypeKind _               = False
 
@@ -146,6 +160,12 @@ 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
@@ -158,10 +178,7 @@ okArrowArgKindCon kc
   | isConstraintKindCon   kc = True
   | otherwise                = False
 
-okArrowResultKindCon kc
-  | okArrowArgKindCon kc = True
-  | isUbxTupleKindCon kc = True
-  | otherwise            = False
+okArrowResultKindCon = okArrowArgKindCon
 
 okArrowArgKind, okArrowResultKind :: Kind -> Bool
 okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
@@ -174,29 +191,21 @@ 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 argTypeKind
+-- 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
-  =  isSubArgTypeKindCon kc
-  || isUbxTupleKindCon   kc
-  || isOpenTypeKindCon   kc
-
-isSubArgTypeKindCon kc
-  =  isUnliftedTypeKindCon kc
+  =  isOpenTypeKindCon   kc
+  || isUnliftedTypeKindCon kc
   || isLiftedTypeKindCon   kc  
-  || isArgTypeKindCon      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
-
-isSubArgTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of ArgTypeKind 
-isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
-isSubArgTypeKind _                = False
+                              -- See Note [Kind Constraint and kind *]
 
 -- | Is this a kind (i.e. a type-of-types)?
 isKind :: Kind -> Bool
@@ -204,60 +213,61 @@ 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
 
-isSuperKindTyCon :: TyCon -> Bool
-isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
-
-isSubKind (FunTy a1 r1) (FunTy a2 r2)
-  = (isSubKind a2 a1) && (isSubKind r1 r2)
-
+-- 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)
-  | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
+  | isPromotedTyCon kc1 || isPromotedTyCon kc2
     -- handles promoted kinds (List *, Nat, etc.)
   = eqKind k1 k2
 
-  | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
-    -- handles BOX
-  = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
-             && null k1s && null k2s, 
-             ppr kc1 <+> ppr kc2 )
-    True   -- If one is BOX, the other must be too
-
-  | 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 )
+    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
-  | isArgTypeKindCon  kc2 = isSubArgTypeKindCon  kc1
-  | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 
-  | 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 not
+-- 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
 
 -------------------------
@@ -281,7 +291,6 @@ defaultKind :: Kind -> Kind
 -- The test is really whether the kind is strictly above '*'
 defaultKind (TyConApp kc _args)
   | isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
-  | isArgTypeKindCon  kc = ASSERT( null _args ) liftedTypeKind
 defaultKind k = k
 
 -- Returns the free kind variables in a kind