From 5653634ead7a7f31f1a584483e53b23e78b047c2 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Mon, 18 Sep 2006 18:16:21 +0000 Subject: [PATCH] Partial changes for derived newtype instances Sat Aug 5 21:16:57 EDT 2006 Manuel M T Chakravarty * Partial changes for derived newtype instances Fri Jul 7 05:45:15 EDT 2006 simonpj@microsoft.com --- compiler/hsSyn/HsBinds.lhs | 3 +- compiler/typecheck/TcDeriv.lhs | 6 +- compiler/typecheck/TcInstDcls.lhs | 115 +++++++++++++++++++++++-------------- compiler/types/TyCon.lhs | 14 +++++ 4 files changed, 92 insertions(+), 46 deletions(-) diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs index 940b6d3..8f9279e 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 65c425d..0a8a498 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 0454e34..cf27ead 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 479ea7c..c80e3a7 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 -- 1.7.10.4