[commit: ghc] wip/impredicativity: Rename and give right kind to (<~) (52b6048)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/impredicativity
Link       : http://ghc.haskell.org/trac/ghc/changeset/52b6048ec7b88baa5e86389d54cf1cfb65947d2a/ghc

>---------------------------------------------------------------

commit 52b6048ec7b88baa5e86389d54cf1cfb65947d2a
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Fri Jul 10 15:26:30 2015 +0200

    Rename and give right kind to (<~)
    
    - Since (<=) is already taken in base, the name of the "instance of"
      constraint has been changed to (<~). It tries to be like "less than
      or equal" where equality is ~.
    - The previous definition of (<=) had kind * -> * -> Constraint.
      This disallows having constraints like Int# <~ Int#, which are
      generated when working with unboxed types. Now, the constraint
      takes arguments of kind OpenKind.


>---------------------------------------------------------------

52b6048ec7b88baa5e86389d54cf1cfb65947d2a
 compiler/coreSyn/CoreSubst.hs   | 15 ++++++---------
 compiler/prelude/TysWiredIn.hs  | 22 ++++++++++++----------
 libraries/ghc-prim/GHC/Types.hs |  6 +++---
 3 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index 89e293a..46975bb 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -57,7 +57,7 @@ import Coercion hiding ( substTy, substCo, extendTvSubst, substTyVarBndr, substC
 import TyCon       ( tyConArity )
 import DataCon
 import PrelNames   ( eqBoxDataConKey, coercibleDataConKey, unpackCStringIdKey
-                   , unpackCStringUtf8IdKey )
+                   , unpackCStringUtf8IdKey, instanceOfTyConKey )
 import OptCoercion ( optCoercion )
 import PprCore     ( pprCoreBindings, pprRules )
 import Module      ( Module )
@@ -959,14 +959,6 @@ simple_app subst (Var v) as
   , isAlwaysActive (idInlineActivation v)
   -- See Note [Unfold compulsory unfoldings in LHSs]
   =  simple_app subst (unfoldingTemplate (idUnfolding v)) as
-  -- Instantiation functions are always inlined
-  {-
-  | lookupIdIsInstantiationFn subst v, isLocalId v, c:cs <- as
-  = case lookupIdSubst (text "simpleOptExpr") subst v of
-      Lam b e -> simple_app (extendIdSubst subst b c) e cs
-      Var v' | v == v' -> foldl App (simple_opt_expr subst e) as
-      e' -> simple_app subst e' as
-  -}
 simple_app subst (Tick t e) as
   -- Okay to do "(Tick t e) x ==> Tick t (e x)"?
   | t `tickishScopesLike` SoftScope
@@ -1031,6 +1023,11 @@ maybe_substitute subst b r
   , not (isUnLiftedType (idType b)) || exprOkForSpeculation r
   = Just (extendIdSubst subst b r)
 
+  | isId b
+  , Just (tc, _) <- splitTyConApp_maybe (idType b)
+  , tc `hasKey` instanceOfTyConKey
+  = Just (extendIdSubst subst b r)  -- Aggresively inline (<=) coercions
+
   | otherwise
   = Nothing
   where
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index d5b0b78..8d538ef 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -188,7 +188,7 @@ coercibleDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "MkCoerc
 
 -- See Note [Kind-changing of (~). Coercible and InstanceOf]
 instanceOfTyConName, instanceOfDataConName, instanceOfAxiomName :: Name
-instanceOfTyConName   = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "<=")   instanceOfTyConKey   instanceOfTyCon
+instanceOfTyConName   = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "<~")   instanceOfTyConKey   instanceOfTyCon
 instanceOfDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "InstOf") instanceOfDataConKey instanceOfDataCon
 instanceOfAxiomName   = mkWiredInName gHC_TYPES (mkDataOccFS (fsLit "InstOfArrow")) instanceOfAxiomKey
                                       (ACoAxiom (toBranchedAxiom instanceOfNewtypeAxiom)) UserSyntax
@@ -597,15 +597,17 @@ coercibleClass = mkClass (tyConTyVars coercibleTyCon) [] [] [] [] [] (mkAnd [])
 
 instanceOfTyCon :: TyCon
 instanceOfTyCon = mkAlgTyCon instanceOfTyConName
-    (mkArrowKinds [liftedTypeKind, liftedTypeKind] constraintKind)
-    [alphaTyVar, betaTyVar]
+    (mkArrowKinds [openTypeKind, openTypeKind] constraintKind)
+    [openAlphaTyVar, openBetaTyVar]
     [Nominal, Nominal]
     Nothing
     []      -- No stupid theta
     (NewTyCon { data_con = instanceOfDataCon
-              , nt_rhs = FunTy (mkTyVarTy alphaTyVar) (mkTyVarTy betaTyVar)
-              , nt_etad_rhs = ( [alphaTyVar, betaTyVar]
-                              , FunTy (mkTyVarTy alphaTyVar) (mkTyVarTy betaTyVar) )
+              , nt_rhs = FunTy (mkTyVarTy openAlphaTyVar)
+                               (mkTyVarTy openBetaTyVar)
+              , nt_etad_rhs = ( [openAlphaTyVar, betaTyVar]
+                              , FunTy (mkTyVarTy openAlphaTyVar)
+                                      (mkTyVarTy openBetaTyVar) )
               , nt_co = instanceOfNewtypeAxiom })
     NoParentTyCon
     NonRecursive
@@ -614,14 +616,14 @@ instanceOfTyCon = mkAlgTyCon instanceOfTyConName
 
 instanceOfDataCon :: DataCon
 instanceOfDataCon = pcDataCon instanceOfDataConName
-    [alphaTyVar, betaTyVar]
-    [FunTy (mkTyVarTy alphaTyVar) (mkTyVarTy betaTyVar)]
+    [openAlphaTyVar, openBetaTyVar]
+    [FunTy (mkTyVarTy openAlphaTyVar) (mkTyVarTy openBetaTyVar)]
     instanceOfTyCon
 
 instanceOfNewtypeAxiom :: CoAxiom Unbranched
 instanceOfNewtypeAxiom = mkNewTypeCo instanceOfAxiomName
-    instanceOfTyCon [alphaTyVar, betaTyVar] [Nominal, Nominal]
-    (FunTy (mkTyVarTy alphaTyVar) (mkTyVarTy betaTyVar))
+    instanceOfTyCon [openAlphaTyVar, openBetaTyVar] [Nominal, Nominal]
+    (FunTy (mkTyVarTy openAlphaTyVar) (mkTyVarTy openBetaTyVar))
 
 charTy :: Type
 charTy = mkTyConTy charTyCon
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 3a9ffaf..f796ebf 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE MagicHash, NoImplicitPrelude, TypeFamilies, UnboxedTuples,
-             MultiParamTypeClasses, RoleAnnotations #-}
+             MultiParamTypeClasses, RoleAnnotations, TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.Types
@@ -24,7 +24,7 @@ module GHC.Types (
         SPEC(..),
         Nat, Symbol,
         Coercible,
-        InstanceOf
+        type (<~)
     ) where
 
 import GHC.Prim
@@ -177,7 +177,7 @@ data Coercible a b = MkCoercible ((~#) a b)
 -- Also see Note [Kind-changing of (~) and Coercible]
 
 -- | A constraint inhabited only if type `a` is an instance of type `b`.
-newtype (<=) b a = InstOf (b -> a)
+newtype (<~) b a = InstOf (b -> a)
 
 -- | Alias for 'tagToEnum#'. Returns True if its parameter is 1# and False
 --   if it is 0#.