Add equality superclasses

Hurrah.  At last we can write

   class (F a ~ b) => C a b where { ... }

This fruit of the fact that equalities are now values,
and all evidence is handled uniformly.

The main tricky point is that when translating to Core
an evidence variable 'v' is represented either as
  either   Var v
  or       Coercion (CoVar v)
depending on whether or not v is an equality.  This leads
to a few annoying calls to 'varToCoreExpr'.

6 files changed, 92 insertions, 95 deletions

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index a6260f40cf..bf58c5ac19 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -487,7 +487,9 @@ mkDictSelId no_unf name clas
     rhs = mkLams tyvars  (Lam dict_id   rhs_body)
     rhs_body | new_tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
              | otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
-                                [(DataAlt data_con, arg_ids, Var the_arg_id)]
+                                [(DataAlt data_con, arg_ids, varToCoreExpr the_arg_id)]
+				-- varToCoreExpr needed for equality superclass selectors
+				--   sel a b d = case x of { MkC _ (g:a~b) _ -> CO g }
 
 dictSelRule :: Int -> Arity 
             -> IdUnfoldingFun -> [CoreExpr] -> Maybe CoreExpr
diff --git a/compiler/deSugar/DsExpr.lhs b/compiler/deSugar/DsExpr.lhs
index e33b113ae7..11eedbe496 100644
--- a/compiler/deSugar/DsExpr.lhs
+++ b/compiler/deSugar/DsExpr.lhs
@@ -217,7 +217,7 @@ dsLExpr (L loc e) = putSrcSpanDs loc $ dsExpr e
 dsExpr :: HsExpr Id -> DsM CoreExpr
 dsExpr (HsPar e) 	      = dsLExpr e
 dsExpr (ExprWithTySigOut e _) = dsLExpr e
-dsExpr (HsVar var)     	      = return (Var var)
+dsExpr (HsVar var)     	      = return (varToCoreExpr var)   -- See Note [Desugaring vars]
 dsExpr (HsIPVar ip)    	      = return (Var (ipNameName ip))
 dsExpr (HsLit lit)     	      = dsLit lit
 dsExpr (HsOverLit lit) 	      = dsOverLit lit
@@ -239,6 +239,22 @@ dsExpr (HsApp fun arg)
   = mkCoreAppDs <$> dsLExpr fun <*>  dsLExpr arg
 \end{code}
 
+Note [Desugaring vars]
+~~~~~~~~~~~~~~~~~~~~~~
+In one situation we can get a *coercion* variable in a HsVar, namely
+the support method for an equality superclass:
+   class (a~b) => C a b where ...
+   instance (blah) => C (T a) (T b) where ..
+Then we get
+   $dfCT :: forall ab. blah => C (T a) (T b)
+   $dfCT ab blah = MkC ($c$p1C a blah) ($cop a blah)
+
+   $c$p1C :: forall ab. blah => (T a ~ T b)
+   $c$p1C ab blah = let ...; g :: T a ~ T b = ... } in g
+
+That 'g' in the 'in' part is an evidence variable, and when
+converting to core it must become a CO.
+   
 Operator sections.  At first it looks as if we can convert
 \begin{verbatim}
 	(expr op)
diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index eabe8c45aa..b9a6ab9352 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -30,7 +30,7 @@ import Type
 import Coercion
 
 import TcRnMonad
-import Data.List	( partition )
+import Util		( isSingleton )
 import Outputable
 \end{code}
 	
@@ -248,12 +248,9 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	; op_items <- mapM (mk_op_item rec_clas) sig_stuff
 	  		-- Build the selector id and default method id
 
-	; let (eq_theta, dict_theta) = partition isEqPred sc_theta
-
-	      -- We only make selectors for the *value* superclasses, 
-	      -- not equality predicates 
+	      -- Make selectors for the superclasses 
 	; sc_sel_names <- mapM  (newImplicitBinder class_name . mkSuperDictSelOcc) 
-				[1..length dict_theta]
+				[1..length sc_theta]
         ; let sc_sel_ids = [ mkDictSelId no_unf sc_name rec_clas 
                            | sc_name <- sc_sel_names]
 	      -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we 
@@ -264,22 +261,23 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	      -- (We used to call them D_C, but now we can have two different
 	      --  superclasses both called C!)
 	
-	; let use_newtype = null eq_theta && (length dict_theta + length sig_stuff == 1)
-		-- Use a newtype if the data constructor has 
-		-- 	(a) exactly one value field
-		--	(b) no existential or equality-predicate fields
-		-- i.e. exactly one operation or superclass taken together
+	; let use_newtype = isSingleton arg_tys && not (any isEqPred sc_theta)
+		-- Use a newtype if the data constructor 
+		--   (a) has exactly one value field
+		--       i.e. exactly one operation or superclass taken together
+                --   (b) it's of lifted type 
+		-- (NB: for (b) don't look at the classes in sc_theta, because
+		--      they are part of the knot!  Hence isEqPred.)
 		-- See note [Class newtypes and equality predicates]
 
-		-- We play a bit fast and loose by treating the dictionary
-		-- superclasses as ordinary arguments.  That means that in 
-                -- the case of
+		-- We treat the dictionary superclasses as ordinary arguments.  
+                -- That means that in the case of
 		--     class C a => D a
 		-- we don't get a newtype with no arguments!
 	      args      = sc_sel_names ++ op_names
 	      op_tys	= [ty | (_,_,ty) <- sig_stuff]
 	      op_names  = [op | (op,_,_) <- sig_stuff]
-	      arg_tys   = map mkPredTy dict_theta ++ op_tys
+	      arg_tys   = map mkPredTy sc_theta ++ op_tys
               rec_tycon = classTyCon rec_clas
                
 	; dict_con <- buildDataCon datacon_name
@@ -288,7 +286,7 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 				   [{- No fields -}]
 				   tvs [{- no existentials -}]
                                    [{- No GADT equalities -}] 
-                                   eq_theta
+                                   [{- No theta -}]
                                    arg_tys
 				   (mkTyConApp rec_tycon (mkTyVarTys tvs))
 				   rec_tycon
@@ -312,9 +310,7 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	      ; atTyCons = [tycon | ATyCon tycon <- ats]
 
 	      ; result = mkClass class_name tvs fds 
-			         (eq_theta ++ dict_theta)  -- Equalities first
-                                 (length eq_theta)	   -- Number of equalities
-                                 sc_sel_ids atTyCons
+			         sc_theta sc_sel_ids atTyCons
 				 op_items tycon
 	      }
 	; traceIf (text "buildClass" <+> ppr tycon) 
@@ -339,12 +335,12 @@ Consider
 	  op :: a -> b
 
 We cannot represent this by a newtype, even though it's not
-existential, and there's only one value field, because we do
-capture an equality predicate:
-
-	data C a b where
-	  MkC :: forall a b. (a ~ F b) => (a->b) -> C a b
-
-We need to access this equality predicate when we get passes a C
-dictionary.  See Trac #2238
+existential, because there are two value fields (the equality
+predicate and op. See Trac #2238
+
+Moreover, 
+	  class (a ~ F b) => C a b where {}
+Here we can't use a newtype either, even though there is only
+one field, because equality predicates are unboxed, and classes
+are boxed.
 
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index b641d23075..33ad0f0f87 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -34,10 +34,10 @@ import DataCon
 import Class
 import Var
 import Pair
-import VarSet
+--import VarSet
 import CoreUtils  ( mkPiTypes )
 import CoreUnfold ( mkDFunUnfolding )
-import CoreSyn    ( Expr(Var), DFunArg(..), CoreExpr )
+import CoreSyn    ( Expr(Var), DFunArg(..), CoreExpr, varToCoreExpr )
 import Id
 import MkId
 import Name
@@ -824,27 +824,34 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
        ; self_dict <- newEvVar (ClassP clas inst_tys)
        ; let class_tc      = classTyCon clas
              [dict_constr] = tyConDataCons class_tc
-             dict_bind     = mkVarBind self_dict dict_rhs
-             dict_rhs      = foldl mk_app inst_constr $
-                             map wrap_sc sc_args 
-                             ++ map (wrapId arg_wrapper) meth_ids
-             wrap_sc (DFunPolyArg (Var sc))  = wrapId arg_wrapper sc
-             wrap_sc (DFunConstArg (Var sc)) = HsVar sc
-	     wrap_sc _ = panic "wrap_sc"
-
-             inst_constr = L loc $ wrapId (mkWpTyApps inst_tys)
-                                          (dataConWrapId dict_constr)
+             dict_bind     = mkVarBind self_dict (L loc con_app_args)
+
                      -- We don't produce a binding for the dict_constr; instead we
                      -- rely on the simplifier to unfold this saturated application
                      -- We do this rather than generate an HsCon directly, because
                      -- it means that the special cases (e.g. dictionary with only one
                      -- member) are dealt with by the common MkId.mkDataConWrapId 
 		     -- code rather than needing to be repeated here.
-
-             mk_app :: LHsExpr Id -> HsExpr Id -> LHsExpr Id
-             mk_app fun arg = L loc (HsApp fun (L loc arg))
-
-             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps (mkTyVarTys inst_tyvars)
+		     --    con_app_tys  = MkD ty1 ty2
+		     --    con_app_scs  = MkD ty1 ty2 sc1 sc2
+		     --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
+             con_app_tys  = wrapId (mkWpTyApps inst_tys)
+                                   (dataConWrapId dict_constr)
+             con_app_scs  = mkHsWrap (mkWpEvApps (map mk_sc_ev_term sc_args)) con_app_tys
+             con_app_args = foldl mk_app con_app_scs $
+                            map (wrapId arg_wrapper) meth_ids
+
+             mk_app :: HsExpr Id -> HsExpr Id -> HsExpr Id
+             mk_app fun arg = HsApp (L loc fun) (L loc arg)
+
+	     mk_sc_ev_term :: EvVar -> EvTerm
+             mk_sc_ev_term sc 
+               | null inst_tv_tys
+               , null dfun_ev_vars = evVarTerm sc
+               | otherwise         = EvDFunApp sc inst_tv_tys dfun_ev_vars
+
+	     inst_tv_tys    = mkTyVarTys inst_tyvars
+             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
 
 	        -- Do not inline the dfun; instead give it a magic DFunFunfolding
 	        -- See Note [ClassOp/DFun selection]
@@ -853,9 +860,12 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                 | isNewTyCon class_tc
                 = dfun_id `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
                 | otherwise
-                = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_ty (sc_args ++ meth_args)
+                = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_ty dfun_args
                           `setInlinePragma` dfunInlinePragma
-             meth_args = map (DFunPolyArg . Var) meth_ids
+
+             dfun_args :: [DFunArg CoreExpr]
+             dfun_args = map (DFunPolyArg . varToCoreExpr) sc_args ++
+                         map (DFunPolyArg . Var) meth_ids
 
              main_bind = AbsBinds { abs_tvs = inst_tyvars
                                   , abs_ev_vars = dfun_ev_vars
@@ -876,22 +886,14 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
 ------------------------------
 tcSuperClass :: [TcTyVar] -> [EvVar] 
 	     -> (Id, PredType) 
-             -> TcM (DFunArg CoreExpr, LHsBinds Id)
+             -> TcM (TcId, LHsBinds TcId)
 
--- For a constant superclass (no free tyvars)
---   return    sc_dict, no bindings, DFunConstArg
--- For a non-constant superclass
--- build a top level decl like
+-- Build a top level decl like
 --	sc_op = /\a \d. let sc = ... in
 --			sc
--- and return sc_op, that binding, DFunPolyArg
+-- and return sc_op, that binding
 
 tcSuperClass tyvars ev_vars (sc_sel, sc_pred)
-  | isEmptyVarSet (tyVarsOfPred sc_pred)  -- Constant
-  = do { sc_dict  <- emitWanted ScOrigin sc_pred
-       ; return (DFunConstArg (Var sc_dict), emptyBag) }
-
-  | otherwise
   = do { (ev_binds, sc_dict)
              <- newImplication InstSkol tyvars ev_vars $
                 emitWanted ScOrigin sc_pred
@@ -901,14 +903,12 @@ tcSuperClass tyvars ev_vars (sc_sel, sc_pred)
 	     sc_op_name = mkDerivedInternalName mkClassOpAuxOcc uniq
 						(getName sc_sel)
 	     sc_op_id   = mkLocalId sc_op_name sc_op_ty
-	     sc_op_bind = VarBind { var_id = sc_op_id, var_inline = False
-                                  , var_rhs = L noSrcSpan $ wrapId sc_wrapper sc_dict }
+	     sc_op_bind = mkVarBind sc_op_id (L noSrcSpan $ wrapId sc_wrapper sc_dict)
              sc_wrapper = mkWpTyLams tyvars
                           <.> mkWpLams ev_vars
 			  <.> mkWpLet ev_binds
-	     binds = unitBag (noLoc sc_op_bind)
 
-       ; return (DFunPolyArg (Var sc_op_id), binds) }
+       ; return (sc_op_id, unitBag sc_op_bind) }
 
 ------------------------------
 tcSpecInstPrags :: DFunId -> InstBindings Name
@@ -1097,14 +1097,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                  rhs = HsWrap (mkWpEvVarApps [self_dict] <.> mkWpTyApps inst_tys) $
     		         HsVar dm_id 
 
-    	         meth_bind = L loc $ VarBind { var_id = local_meth_id
-                                             , var_rhs = L loc rhs 
-                                             , var_inline = False }
+    	         meth_bind = mkVarBind local_meth_id (L loc rhs)
                  meth_id1 = meth_id `setInlinePragma` dm_inline_prag
-    		   	    -- Copy the inline pragma (if any) from the default
-    			    -- method to this version. Note [INLINE and default methods]
+    		   	-- Copy the inline pragma (if any) from the default
+    			-- method to this version. Note [INLINE and default methods]
     			    
-                 bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars =  dfun_ev_vars
+                 bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
                                  , abs_exports = [( tyvars, meth_id1, local_meth_id
                                                   , mk_meth_spec_prags meth_id1 [])]
                                  , abs_ev_binds = EvBinds (unitBag self_ev_bind)
@@ -1198,15 +1196,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                                                     inst_tys sel_id
 
             ; let meth_rhs  = wrapId (mk_op_wrapper sel_id rep_d) sel_id
-                  meth_bind = VarBind { var_id = local_meth_id
-                                      , var_rhs = L loc meth_rhs
-    				      , var_inline = False }
-
+                  meth_bind = mkVarBind local_meth_id (L loc meth_rhs)
 	          bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
                                    , abs_exports = [(tyvars, meth_id, 
                                                      local_meth_id, noSpecPrags)]
 				   , abs_ev_binds = rep_ev_binds
-                                   , abs_binds = unitBag $ L loc meth_bind }
+                                   , abs_binds = unitBag $ meth_bind }
 
             ; return (meth_id, L loc bind) }
 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 06d4596d35..ef7ecdc64e 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1139,13 +1139,11 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
 
 
-check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+check_pred_ty dflags _ctxt pred@(EqPred ty1 ty2)
   = do {	-- Equational constraints are valid in all contexts if type
 		-- families are permitted
        ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) 
                  (eqPredTyErr pred)
-       ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
-                 (eqSuperClassErr pred)
 
 		-- Check the form of the argument types
        ; checkValidMonoType ty1
@@ -1302,11 +1300,6 @@ checkThetaCtxt ctxt theta
   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
 	  ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
 
-eqSuperClassErr :: PredType -> SDoc
-eqSuperClassErr pred
-  = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
-       2 (ppr pred)
-
 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
 eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
diff --git a/compiler/types/Class.lhs b/compiler/types/Class.lhs
index d9e44e591c..8f8ff3bd5a 100644
--- a/compiler/types/Class.lhs
+++ b/compiler/types/Class.lhs
@@ -13,7 +13,7 @@ module Class (
 
 	FunDep,	pprFundeps, pprFunDep,
 
-	mkClass, classTyVars, classArity, classSCNEqs,
+	mkClass, classTyVars, classArity, 
 	classKey, className, classATs, classTyCon, classMethods,
 	classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
         classAllSelIds, classSCSelId
@@ -57,15 +57,13 @@ data Class
         -- We need value-level selectors for the dictionary 
 	-- superclasses, but not for the equality superclasses
 	classSCTheta :: [PredType],	-- Immediate superclasses, 
-		     			---   *with equalities first*
-        classSCNEqs  :: Int,		-- How many equalities
 	classSCSels  :: [Id],		-- Selector functions to extract the
-		     			--   *dictionary* superclasses from a 
+		     			--   superclasses from a 
 					--   dictionary of this class
 	-- Associated types
         classATs     :: [TyCon],	-- Associated type families
 
-        -- Class operations
+        -- Class operations (methods, not superclasses)
 	classOpStuff :: [ClassOpItem],	-- Ordered by tag
 
 	classTyCon :: TyCon		-- The data type constructor for
@@ -100,20 +98,19 @@ The @mkClass@ function fills in the indirect superclasses.
 \begin{code}
 mkClass :: Name -> [TyVar]
 	-> [([TyVar], [TyVar])]
-	-> [PredType] -> Int -> [Id]
+	-> [PredType] -> [Id]
 	-> [TyCon]
 	-> [ClassOpItem]
 	-> TyCon
 	-> Class
 
-mkClass name tyvars fds super_classes n_eqs superdict_sels ats 
+mkClass name tyvars fds super_classes superdict_sels ats 
 	op_stuff tycon
   = Class {	classKey     = getUnique name, 
 		className    = name,
 		classTyVars  = tyvars,
 		classFunDeps = fds,
 		classSCTheta = super_classes,
-                classSCNEqs  = n_eqs,
 		classSCSels  = superdict_sels,
 		classATs     = ats,
 		classOpStuff = op_stuff,
@@ -142,11 +139,9 @@ classSCSelId :: Class -> Int -> Id
 -- Get the n'th superclass selector Id
 -- where n is 0-indexed, and counts 
 --    *all* superclasses including equalities
-classSCSelId (Class { classSCNEqs = n_eqs, classSCSels = sc_sels }) n
-  = ASSERT( sc_sel_index >= 0 && sc_sel_index < length sc_sels )
-    sc_sels !! sc_sel_index
-  where
-    sc_sel_index = n - n_eqs	-- 0-index into classSCSels
+classSCSelId (Class { classSCSels = sc_sels }) n
+  = ASSERT( n >= 0 && n < length sc_sels )
+    sc_sels !! n
 
 classMethods :: Class -> [Id]
 classMethods (Class {classOpStuff = op_stuff})