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

diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index 940b6d3..8f9279e 100644 (file)
--- 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 65c425d..0a8a498 100644 (file)
--- 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 0454e34..cf27ead 100644 (file)
--- 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 479ea7c..c80e3a7 100644 (file)
--- 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