Make Constraint and * look identical in Core (System FC)

Fixes Trac #7451. See Note [Kind Constraint and kind *] in Kind.lhs.

Conflicts:
	compiler/types/Kind.lhs
	compiler/types/Type.lhs

compiler/iface/IfaceType.lhs

@@ -195,7 +195,7 @@ pprParendIfaceType = ppr_ty tYCON_PREC
 isIfacePredTy :: IfaceType -> Bool
 isIfacePredTy _  = False
 -- FIXME: fix this to print iface pred tys correctly
--- isIfacePredTy ty = ifaceTypeKind ty `eqKind` constraintKind
+-- isIfacePredTy ty = isConstraintKind (ifaceTypeKind ty)
 
 ppr_ty :: Int -> IfaceType -> SDoc
 ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar

compiler/types/Kind.lhs

@@ -70,6 +70,30 @@ import Util
 %*									*
 %************************************************************************
 
+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.
+
+Howver, 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 
+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
@@ -111,7 +135,7 @@ isOpenTypeKind, isUnliftedTypeKind,
 
 isOpenTypeKindCon, isUnliftedTypeKindCon,
   isSubOpenTypeKindCon, isConstraintKindCon,
-  isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool
+  isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
 
 
 isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
@@ -119,6 +143,7 @@ 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
@@ -167,7 +192,7 @@ 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
@@ -180,6 +205,7 @@ isSubOpenTypeKindCon 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
@@ -187,37 +213,29 @@ isKind k = isSuperKind (typeKind k)
 
 isSubKind :: Kind -> Kind -> Bool
 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
-
-isSuperKindTyCon :: TyCon -> Bool
-isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
-
-isSubKind (FunTy a1 r1) (FunTy a2 r2)
-  = (isSubKind a2 a1) && (isSubKind r1 r2)
+-- Sub-kinding is extremely simple and does not look
+-- under arrrows or type constructors
 
 isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
   | 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@
 isSubKindCon kc1 kc2
-  | kc1 == kc2            = True
-  | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 
-  | otherwise             = False
+  | kc1 == kc2              = True
+  | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 
+  | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
+  | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
+  | otherwise               = False
+    -- See Note [Kind Constraint and kind *]
 
 -------------------------
 -- Hack alert: we need a tiny variant for the typechecker

compiler/types/Type.lhs

@@ -151,10 +151,9 @@ import Class
 import TyCon
 import TysPrim
 import {-# SOURCE #-} TysWiredIn ( eqTyCon, mkBoxedTupleTy )
-import PrelNames	         ( eqTyConKey, ipClassName )
+import PrelNames
 
 -- others
-import Unique		( Unique, hasKey )
 import BasicTypes	( Arity, RepArity )
 import NameSet
 import StaticFlags
@@ -842,7 +841,7 @@ noParenPred p = not (isIPPred p) && isClassPred p || isEqPred p
 isPredTy :: Type -> Bool
 isPredTy ty
   | isSuperKind ty = False
-  | otherwise = typeKind ty `eqKind` constraintKind
+  | otherwise = isConstraintKind (typeKind ty)
 
 isKindTy :: Type -> Bool
 isKindTy = isSuperKind . typeKind
@@ -1223,7 +1222,7 @@ cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX env (tyVarKind t
                                                        `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
-cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
+cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2
 cmpTypeX _   (LitTy l1)          (LitTy l2)          = compare l1 l2
 
     -- Deal with the rest: TyVarTy < AppTy < FunTy < LitTy < TyConApp < ForAllTy < PredTy
@@ -1255,6 +1254,17 @@ cmpTypesX _   []        []        = EQ
 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
 cmpTypesX _   []        _         = LT
 cmpTypesX _   _         []        = GT
+
+-------------
+cmpTc :: TyCon -> TyCon -> Ordering
+-- Here we treat * and Constraint as equal
+-- See Note [Kind Constraint and kind *] in Kinds.lhs
+cmpTc tc1 tc2 = nu1 `compare` nu2
+  where
+    u1  = tyConUnique tc1
+    nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1
+    u2  = tyConUnique tc2
+    nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2
 \end{code}
 
 Note [cmpTypeX]