Commit 5653634e authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

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
parent ad0e3c1e
......@@ -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("<>")
......
......@@ -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
......
......@@ -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}
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment