Updated documentation; changed "group" to "branched" in type families
[ghc.git] / compiler / types / Kind.lhs
index 6ce2dd9..0082a33 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The University of Glasgow 2006
+% (c) The University of Glasgow 2006-2012
 %
 
 \begin{code}
@@ -17,7 +17,6 @@ module Kind (
        -- Kinds
        anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind,
         mkArrowKind, mkArrowKinds,
-        typeNatKind, typeStringKind,
 
         -- Kind constructors...
         anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
@@ -80,11 +79,11 @@ The special thing about types of kind Constraint is that
    engine inserts an extra argument of type (Ord a) at every call site
    to f.
 
-Howver, once type inference is over, there is *no* distinction between 
+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 genreate a newtype, which in turn 
+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 *.
@@ -217,6 +216,8 @@ isSubKind :: Kind -> Kind -> Bool
 -- Sub-kinding is extremely simple and does not look
 -- under arrrows or type constructors
 
+-- 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.)
@@ -230,35 +231,43 @@ 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
   | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 
   | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
   | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
-  | otherwise               = False
     -- 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
 
 -------------------------