Partial changes for derived newtype instances

Sat Aug  5 21:16:57 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Partial changes for derived newtype instances
  Fri Jul  7 05:45:15 EDT 2006  simonpj@microsoft.com

4 files changed, 92 insertions, 46 deletions

diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index 940b6d3e24..8f9279e923 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -316,7 +316,8 @@ data ExprCoFn
   | CoTyApps [Type]		-- [] t1 .. tn
   | CoLams [Id] 		-- \x1..xn. []; the xi are dicts or coercions
   | CoTyLams [TyVar] 		-- \a1..an. []
-  | CoLet (LHsBinds Id)		-- Would be nicer to be core bindings
+  | CoLet (LHsBinds Id)		-- let binds in []
+				-- (ould be nicer to be core bindings)
 
 instance Outputable ExprCoFn where
   ppr CoHole	     = ptext SLIT("<>")
diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index 65c425d255..0a8a498232 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -350,6 +350,10 @@ makeDerivEqns overlap_flag tycl_decls
         mk_eqn_help gla_exts new_or_data tycon deriv_tvs clas tys
 
     ------------------------------------------------------------------
+    -- data/newtype T a = ... deriving( C t1 t2 )
+    --   leads to a call to mk_eqn_help with
+    --		tycon = T, deriv_tvs = ftv(t1,t2), clas = C, tys = [t1,t2]
+
     mk_eqn_help gla_exts DataType tycon deriv_tvs clas tys
       | Just err <- checkSideConditions gla_exts tycon deriv_tvs clas tys
       = bale_out (derivingThingErr clas tys tycon (tyConTyVars tycon) err)
@@ -434,7 +438,7 @@ makeDerivEqns overlap_flag tycl_decls
 		-- We must pass the superclasses; the newtype might be an instance
 		-- of them in a different way than the representation type
 		-- E.g.		newtype Foo a = Foo a deriving( Show, Num, Eq )
-		-- Then the Show instance is not done via isomprphism; it shows
+		-- Then the Show instance is not done via isomorphism; it shows
 		-- 	Foo 3 as "Foo 3"
 		-- The Num instance is derived via isomorphism, but the Show superclass
 		-- dictionary must the Show instance for Foo, *not* the Show dictionary
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 0454e34832..cf27ead743 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -303,8 +303,75 @@ First comes the easy case of a non-local instance decl.
 
 \begin{code}
 tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
+-- Returns a binding for the dfun
 
-tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds })
+		** Explain superclass stuff ***
+
+-- Derived newtype instances
+-- In the case of a newtype, things are rather easy
+-- 	class Show a => Foo a b where ...
+-- 	newtype T a = MkT (Tree [a]) deriving( Foo Int )
+-- The newtype gives an FC axiom looking like
+--	axiom CoT a :: Tree [a] = T a
+--
+-- So all need is to generate a binding looking like
+-- 	dfunFooT :: forall a. (Show (T a), Foo Int (Tree [a]) => Foo Int (T a)
+--	dfunFooT = /\a. \(ds:Show (T a) (df:Foo (Tree [a])).
+--		  case df `cast` (Foo Int (CoT a)) of
+--		     Foo _ op1 .. opn -> Foo ds op1 .. opn
+
+tcInstDecl2 (InstInfo { iSpec = ispec, 
+			iBinds = NewTypeDerived rep_tys })
+  = do	{ let dfun_id = instanceDFunId ispec 
+	      rigid_info = InstSkol dfun_id
+	      origin	 = SigOrigin rigid_info
+	      inst_ty    = idType dfun_id
+	; (tvs, theta, inst_head) <- tcSkolSigType rigid_info inst_ty
+	; ASSERT( isSingleton theta )	-- Always the case for NewTypeDerived
+	  rep_dict <- newDict origin (head theta)
+
+	; let rep_dict_id = instToId rep_dict
+	      cast = 
+	      co_fn = CoTyLams tvs <.> CoLams [rep_dict_id] <.> ExprCoFn cast
+
+	; return (unitBag (VarBind dfun_id (HsCoerce co_fn (HsVar rep_dict_id))))
+
+tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
+	  avail_insts op_items (NewTypeDerived rep_tys)
+  = getInstLoc origin				`thenM` \ inst_loc ->
+    mapAndUnzip3M (do_one inst_loc) op_items	`thenM` \ (meth_ids, meth_binds, rhs_insts) ->
+    
+    tcSimplifyCheck
+	 (ptext SLIT("newtype derived instance"))
+	 inst_tyvars' avail_insts rhs_insts	`thenM` \ lie_binds ->
+
+	-- I don't think we have to do the checkSigTyVars thing
+
+    returnM (meth_ids, lie_binds `unionBags` listToBag meth_binds)
+
+  where
+    do_one inst_loc (sel_id, _)
+	= -- The binding is like "op @ NewTy = op @ RepTy"
+		-- Make the *binder*, like in mkMethodBind
+	  tcInstClassOp inst_loc sel_id inst_tys'	`thenM` \ meth_inst ->
+
+		-- Make the *occurrence on the rhs*
+	  tcInstClassOp inst_loc sel_id rep_tys'	`thenM` \ rhs_inst ->
+	  let
+	     meth_id = instToId meth_inst
+	  in
+	  return (meth_id, noLoc (VarBind meth_id (nlHsVar (instToId rhs_inst))), rhs_inst)
+
+	-- Instantiate rep_tys with the relevant type variables
+	-- This looks a bit odd, because inst_tyvars' are the skolemised version
+	-- of the type variables in the instance declaration; but rep_tys doesn't
+	-- have the skolemised version, so we substitute them in here
+    rep_tys' = substTys subst rep_tys
+    subst    = zipOpenTvSubst inst_tyvars' (mkTyVarTys inst_tyvars')
+
+
+
+tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
   = let 
 	dfun_id    = instanceDFunId ispec
 	rigid_info = InstSkol dfun_id
@@ -341,7 +408,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds })
     in
     tcMethods origin clas inst_tyvars' 
 	      dfun_theta' inst_tys' avail_insts 
-	      op_items binds		`thenM` \ (meth_ids, meth_binds) ->
+	      op_items monobinds uprags		`thenM` \ (meth_ids, meth_binds) ->
 
 	-- Figure out bindings for the superclass context
 	-- Don't include this_dict in the 'givens', else
@@ -356,12 +423,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds })
     checkSigTyVars inst_tyvars' 	`thenM_`
 
 	-- Deal with 'SPECIALISE instance' pragmas 
-    let
-	specs = case binds of
-		  VanillaInst _ prags -> filter isSpecInstLSig prags
-		  other	 	      -> []
-    in
-    tcPrags dfun_id specs			`thenM` \ prags -> 
+    tcPrags dfun_id (filter isSpecInstLSig prags)	`thenM` \ prags -> 
     
 	-- Create the result bindings
     let
@@ -405,7 +467,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds })
 
 
 tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
-	  avail_insts op_items (VanillaInst monobinds uprags)
+	  avail_insts op_items monobinds uprags
   = 	-- Check that all the method bindings come from this class
     let
 	sel_names = [idName sel_id | (sel_id, _) <- op_items]
@@ -461,41 +523,6 @@ tcMethods origin clas inst_tyvars' dfun_theta' inst_tys'
     mapM tc_method_bind meth_infos		`thenM` \ meth_binds_s ->
    
     returnM (meth_ids, unionManyBags meth_binds_s)
-
-
--- Derived newtype instances
-tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
-	  avail_insts op_items (NewTypeDerived rep_tys)
-  = getInstLoc origin				`thenM` \ inst_loc ->
-    mapAndUnzip3M (do_one inst_loc) op_items	`thenM` \ (meth_ids, meth_binds, rhs_insts) ->
-    
-    tcSimplifyCheck
-	 (ptext SLIT("newtype derived instance"))
-	 inst_tyvars' avail_insts rhs_insts	`thenM` \ lie_binds ->
-
-	-- I don't think we have to do the checkSigTyVars thing
-
-    returnM (meth_ids, lie_binds `unionBags` listToBag meth_binds)
-
-  where
-    do_one inst_loc (sel_id, _)
-	= -- The binding is like "op @ NewTy = op @ RepTy"
-		-- Make the *binder*, like in mkMethodBind
-	  tcInstClassOp inst_loc sel_id inst_tys'	`thenM` \ meth_inst ->
-
-		-- Make the *occurrence on the rhs*
-	  tcInstClassOp inst_loc sel_id rep_tys'	`thenM` \ rhs_inst ->
-	  let
-	     meth_id = instToId meth_inst
-	  in
-	  return (meth_id, noLoc (VarBind meth_id (nlHsVar (instToId rhs_inst))), rhs_inst)
-
-	-- Instantiate rep_tys with the relevant type variables
-	-- This looks a bit odd, because inst_tyvars' are the skolemised version
-	-- of the type variables in the instance declaration; but rep_tys doesn't
-	-- have the skolemised version, so we substitute them in here
-    rep_tys' = substTys subst rep_tys
-    subst    = zipOpenTvSubst inst_tyvars' (mkTyVarTys inst_tyvars')
 \end{code}
 
 
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 479ea7c110..c80e3a7dc7 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -252,6 +252,20 @@ This TyCon is a CoercionTyCon, so it does not have a kind on its own;
 it basically has its own typing rule for the fully-applied version.
 If the newtype T has k type variables then CoT has arity k.
 
+In the paper we'd write
+	axiom CoT : (forall t. [t]) :=: (forall t. T t)
+and then when we used CoT at a particular type, s, we'd say
+	CoT @ s
+which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
+
+But in GHC we instead make CoT into a new piece of type syntax
+(like instCoercionTyCon, symCoercionTyCon etc), which must always
+be saturated, but which encodes as
+	TyConAp CoT [s]
+In the vocabulary of the paper it's as if we had axiom declarations
+like
+	axiom CoT t : ([t] :=: T t)
+
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider