diff options
| -rw-r--r-- | compiler/typecheck/FamInst.lhs | 49 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.lhs | 135 | ||||
| -rw-r--r-- | compiler/typecheck/TcInstDcls.lhs | 43 | ||||
| -rw-r--r-- | compiler/types/FamInstEnv.lhs | 55 |
4 files changed, 163 insertions, 119 deletions
diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index e99133bb84..44a0cefac5 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -11,7 +11,7 @@ The @FamInst@ type: family instance heads module FamInst ( checkFamInstConsistency, tcExtendLocalFamInstEnv, - tcLookupFamInst, tcLookupDataFamInst, + tcLookupFamInst, tcGetFamInstEnvs, newFamInst ) where @@ -231,55 +231,8 @@ tcLookupFamInst tycon tys (match:_) -> return $ Just match } - -tcLookupDataFamInst :: TyCon -> [Type] -> TcM (TyCon, [Type]) --- Find the instance of a data family --- Note [Looking up family instances for deriving] -tcLookupDataFamInst tycon tys - | not (isFamilyTyCon tycon) - = return (tycon, tys) - | otherwise - = ASSERT( isAlgTyCon tycon ) - do { maybeFamInst <- tcLookupFamInst tycon tys - ; case maybeFamInst of - Nothing -> famInstNotFound tycon tys - Just (FamInstMatch { fim_instance = famInst - , fim_index = index - , fim_tys = tys }) - -> ASSERT( index == 0 ) - let tycon' = dataFamInstRepTyCon famInst - in return (tycon', tys) } - -famInstNotFound :: TyCon -> [Type] -> TcM a -famInstNotFound tycon tys - = failWithTc (ptext (sLit "No family instance for") - <+> quotes (pprTypeApp tycon tys)) \end{code} -Note [Looking up family instances for deriving] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -tcLookupFamInstExact is an auxiliary lookup wrapper which requires -that looked-up family instances exist. If called with a vanilla -tycon, the old type application is simply returned. - -If we have - data instance F () = ... deriving Eq - data instance F () = ... deriving Eq -then tcLookupFamInstExact will be confused by the two matches; -but that can't happen because tcInstDecls1 doesn't call tcDeriving -if there are any overlaps. - -There are two other things that might go wrong with the lookup. -First, we might see a standalone deriving clause - deriving Eq (F ()) -when there is no data instance F () in scope. - -Note that it's OK to have - data instance F [a] = ... - deriving Eq (F [(a,b)]) -where the match is not exact; the same holds for ordinary data types -with standalone deriving declrations. - %************************************************************************ %* * diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 786d93ecd8..97a548d24e 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -591,8 +591,8 @@ deriveStandalone (L loc (DerivDecl deriv_ty)) (Just theta) } ------------------------------------------------------------------ -deriveTyData :: [TyVar] -> TyCon -> [Type] - -> LHsType Name -- The deriving predicate +deriveTyData :: [TyVar] -> TyCon -> [Type] -- LHS of data or data instance + -> LHsType Name -- The deriving predicate -> TcM EarlyDerivSpec -- The deriving clause of a data or newtype declaration deriveTyData tvs tc tc_args (L loc deriv_pred) @@ -625,7 +625,7 @@ deriveTyData tvs tc tc_args (L loc deriv_pred) args_to_drop = drop n_args_to_keep tc_args inst_ty = mkTyConApp tc (take n_args_to_keep tc_args) inst_ty_kind = typeKind inst_ty - dropped_tvs = mkVarSet (mapCatMaybes getTyVar_maybe args_to_drop) + dropped_tvs = tyVarsOfTypes args_to_drop univ_tvs = (mkVarSet tvs `extendVarSetList` deriv_tvs) `minusVarSet` dropped_tvs @@ -636,22 +636,19 @@ deriveTyData tvs tc tc_args (L loc deriv_pred) ; checkTc (n_args_to_keep >= 0 && (inst_ty_kind `eqKind` kind)) (derivingKindErr tc cls cls_tys kind) - ; checkTc (sizeVarSet dropped_tvs == n_args_to_drop && -- (a) - tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (b) + ; checkTc (all isTyVarTy args_to_drop && -- (a) + sizeVarSet dropped_tvs == n_args_to_drop && -- (b) + tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (c) (derivingEtaErr cls cls_tys inst_ty) -- Check that + -- (a) The args to drop are all type variables; eg reject: + -- data instance T a Int = .... deriving( Monad ) -- (a) The data type can be eta-reduced; eg reject: -- data instance T a a = ... deriving( Monad ) -- (b) The type class args do not mention any of the dropped type -- variables -- newtype T a s = ... deriving( ST s ) - -- Type families can't be partially applied - -- e.g. newtype instance T Int a = MkT [a] deriving( Monad ) - -- Note [Deriving, type families, and partial applications] - ; checkTc (not (isFamilyTyCon tc) || n_args_to_drop == 0) - (typeFamilyPapErr tc cls cls_tys inst_ty) - ; mkEqnHelp DerivOrigin (varSetElemsKvsFirst univ_tvs) cls cls_tys inst_ty Nothing } } where kindVarsOnly :: [Type] -> [Type] @@ -661,33 +658,6 @@ deriveTyData tvs tc tc_args (L loc deriv_pred) | otherwise = kindVarsOnly ts \end{code} -Note [Deriving, type families, and partial applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When there are no type families, it's quite easy: - - newtype S a = MkS [a] - -- :CoS :: S ~ [] -- Eta-reduced - - instance Eq [a] => Eq (S a) -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a) - instance Monad [] => Monad S -- by coercion sym (Monad :CoS) : Monad [] ~ Monad S - -When type familes are involved it's trickier: - - data family T a b - newtype instance T Int a = MkT [a] deriving( Eq, Monad ) - -- :RT is the representation type for (T Int a) - -- :CoF:R1T a :: T Int a ~ :RT a -- Not eta reduced - -- :Co:R1T :: :RT ~ [] -- Eta-reduced - - instance Eq [a] => Eq (T Int a) -- easy by coercion - instance Monad [] => Monad (T Int) -- only if we can eta reduce??? - -The "???" bit is that we don't build the :CoF thing in eta-reduced form -Henc the current typeFamilyPapErr, even though the instance makes sense. -After all, we can write it out - instance Monad [] => Monad (T Int) -- only if we can eta reduce??? - return x = MkT [x] - ... etc ... \begin{code} mkEqnHelp :: CtOrigin -> [TyVar] -> Class -> [Type] -> Type @@ -704,6 +674,7 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta , className cls == typeableClassName || isAlgTyCon tycon -- Avoid functions, primitive types, etc, unless it's Typeable = mk_alg_eqn tycon tc_args + | otherwise = failWithTc (derivingThingErr False cls cls_tys tc_app (ptext (sLit "The last argument of the instance must be a data or newtype application"))) @@ -722,12 +693,8 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta -- We checked for errors before, so we don't need to do that again = mkPolyKindedTypeableEqn orig tvs cls cls_tys tycon tc_args mtheta - | isDataFamilyTyCon tycon - , length tc_args /= tyConArity tycon - = bale_out (ptext (sLit "Unsaturated data family application")) - | otherwise - = do { (rep_tc, rep_tc_args) <- tcLookupDataFamInst tycon tc_args + = do { (rep_tc, rep_tc_args) <- lookup_data_fam tycon tc_args -- Be careful to test rep_tc here: in the case of families, -- we want to check the instance tycon, not the family tycon @@ -748,8 +715,85 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta else mkNewTypeEqn orig dflags tvs cls cls_tys tycon tc_args rep_tc rep_tc_args mtheta } + + lookup_data_fam :: TyCon -> [Type] -> TcM (TyCon, [Type]) + -- Find the instance of a data family + -- Note [Looking up family instances for deriving] + lookup_data_fam tycon tys + | not (isFamilyTyCon tycon) + = return (tycon, tys) + | otherwise + = ASSERT( isAlgTyCon tycon ) + do { maybeFamInst <- tcLookupFamInst tycon tys + ; case maybeFamInst of + Nothing -> bale_out (ptext (sLit "No family instance for") + <+> quotes (pprTypeApp tycon tys)) + Just (FamInstMatch { fim_instance = famInst + , fim_index = index + , fim_tys = tys }) + -> ASSERT( index == 0 ) + let tycon' = dataFamInstRepTyCon famInst + in return (tycon', tys) } \end{code} +Note [Looking up family instances for deriving] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tcLookupFamInstExact is an auxiliary lookup wrapper which requires +that looked-up family instances exist. If called with a vanilla +tycon, the old type application is simply returned. + +If we have + data instance F () = ... deriving Eq + data instance F () = ... deriving Eq +then tcLookupFamInstExact will be confused by the two matches; +but that can't happen because tcInstDecls1 doesn't call tcDeriving +if there are any overlaps. + +There are two other things that might go wrong with the lookup. +First, we might see a standalone deriving clause + deriving Eq (F ()) +when there is no data instance F () in scope. + +Note that it's OK to have + data instance F [a] = ... + deriving Eq (F [(a,b)]) +where the match is not exact; the same holds for ordinary data types +with standalone deriving declarations. + +Note [Deriving, type families, and partial applications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When there are no type families, it's quite easy: + + newtype S a = MkS [a] + -- :CoS :: S ~ [] -- Eta-reduced + + instance Eq [a] => Eq (S a) -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a) + instance Monad [] => Monad S -- by coercion sym (Monad :CoS) : Monad [] ~ Monad S + +When type familes are involved it's trickier: + + data family T a b + newtype instance T Int a = MkT [a] deriving( Eq, Monad ) + -- :RT is the representation type for (T Int a) + -- :Co:RT :: :RT ~ [] -- Eta-reduced! + -- :CoF:RT a :: T Int a ~ :RT a -- Also eta-reduced! + + instance Eq [a] => Eq (T Int a) -- easy by coercion + -- d1 :: Eq [a] + -- d2 :: Eq (T Int a) = d1 |> Eq (sym (:Co:RT a ; :coF:RT a)) + + instance Monad [] => Monad (T Int) -- only if we can eta reduce??? + -- d1 :: Monad [] + -- d2 :: Monad (T Int) = d1 |> Monad (sym (:Co:RT ; :coF:RT)) + +Note the need for the eta-reduced rule axioms. After all, we can +write it out + instance Monad [] => Monad (T Int) -- only if we can eta reduce??? + return x = MkT [x] + ... etc ... + +See Note [Eta reduction for data family axioms] in TcInstDcls. + %************************************************************************ %* * @@ -1843,11 +1887,6 @@ derivingEtaErr cls cls_tys inst_ty nest 2 (ptext (sLit "instance (...) =>") <+> pprClassPred cls (cls_tys ++ [inst_ty]))] -typeFamilyPapErr :: TyCon -> Class -> [Type] -> Type -> MsgDoc -typeFamilyPapErr tc cls cls_tys inst_ty - = hang (ptext (sLit "Derived instance") <+> quotes (pprClassPred cls (cls_tys ++ [inst_ty]))) - 2 (ptext (sLit "requires illegal partial application of data type family") <+> ppr tc) - derivingThingErr :: Bool -> Class -> [Type] -> Type -> MsgDoc -> MsgDoc derivingThingErr newtype_deriving clas tys ty why = sep [(hang (ptext (sLit "Can't make a derived instance of")) diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index a6f6b3e33c..753bc327be 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -50,7 +50,7 @@ import DataCon import Class import Var import VarEnv -import VarSet ( mkVarSet, subVarSet, varSetElems ) +import VarSet import Pair import CoreUnfold ( mkDFunUnfolding ) import CoreSyn ( Expr(Var, Type), CoreExpr, mkTyApps, mkVarApps ) @@ -712,8 +712,9 @@ tcDataFamInstDecl mb_clsinfo NewType -> ASSERT( not (null data_cons) ) mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons) -- freshen tyvars - ; let axiom = mkSingleCoAxiom axiom_name tvs' fam_tc pats' - (mkTyConApp rep_tc (mkTyVarTys tvs')) + ; let (eta_tvs, eta_pats) = eta_reduce tvs' pats' + axiom = mkSingleCoAxiom axiom_name eta_tvs fam_tc eta_pats + (mkTyConApp rep_tc (mkTyVarTys eta_tvs)) parent = FamInstTyCon axiom fam_tc pats' rep_tc = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs Recursive @@ -730,8 +731,44 @@ tcDataFamInstDecl mb_clsinfo -- Remember to check validity; no recursion to worry about here ; checkValidTyCon rep_tc ; return fam_inst } } + where + -- See Note [Eta reduction for data family axioms] + -- [a,b,c,d].T [a] c Int c d ==> [a,b,c]. T [a] c Int c + eta_reduce tvs pats = go (reverse tvs) (reverse pats) + go (tv:tvs) (pat:pats) + | Just tv' <- getTyVar_maybe pat + , tv == tv' + , not (tv `elemVarSet` tyVarsOfTypes pats) + = go tvs pats + go tvs pats = (reverse tvs, reverse pats) \end{code} +Note [Eta reduction for data family axioms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this + data family T a b :: * + newtype instance T Int a = MkT (IO a) deriving( Monad ) +We'd like this to work. From the 'newtype instance' you might +think we'd get: + newtype TInt a = MkT (IO a) + axiom ax1 a :: T Int a ~ TInt a -- The type-instance part + axiom ax2 a :: TInt a ~ IO a -- The newtype part + +But now what can we do? We have this problem + Given: d :: Monad IO + Wanted: d' :: Monad (T Int) = d |> ???? +What coercion can we use for the ??? + +Solution: eta-reduce both axioms, thus: + axiom ax1 :: T Int ~ TInt + axiom ax2 :: TInt ~ IO +Now + d' = d |> Monad (sym (ax2 ; ax1)) + +See Note [Newtype eta] in TyCon. + + + %************************************************************************ %* * Type-checking instance declarations, pass 2 diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index d7371d6dd7..34f1701354 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -133,10 +133,14 @@ data FamInstBranch -- Like ClsInsts, these variables are always -- fresh. See Note [Template tyvars are fresh] -- in InstEnv - , fib_lhs :: [Type] -- type patterns + + , fib_lhs :: [Type] -- Type patterns + , fib_rhs :: Type -- RHS of family instance -- See Note [Why we need fib_rhs] - , fib_tcs :: [Maybe Name] -- used for "rough matching" during typechecking + + , fib_tcs :: [Maybe Name] -- Used for "rough matching" during typechecking + -- In 1-1 correspondence with fib_lhs -- see Note [Rough-match field] in InstEnv } @@ -316,7 +320,7 @@ mkImportedFamInst fam branched roughs axiom %************************************************************************ Note [FamInstEnv] -~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~ A FamInstEnv maps a family name to the list of known instances for that family. The same FamInstEnv includes both 'data family' and 'type family' instances. @@ -334,6 +338,25 @@ Neverthless it is still useful to have data families in the FamInstEnv: - In standalone deriving instance Eq (T [Int]) we need to find the representation type for T [Int] +Note [Varying number of patterns for data family axioms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For data families, the number of patterns may vary between instances. +For example + data family T a b + data instance T Int a = T1 a | T2 + data instance T Bool [a] = T3 a + +Then we get a data type for each instance, and an axiom: + data TInt a = T1 a | T2 + data TBoolList a = T3 a + + axiom ax7 :: T Int ~ TInt -- Eta-reduced + axiom ax8 a :: T Bool [a] ~ TBoolList a + +These two axioms for T, one with one pattern, one with two. The reason +for this eta-reduction is decribed in TcInstDcls + Note [Eta reduction for data family axioms] + \begin{code} type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances -- See Note [FamInstEnv] @@ -701,21 +724,8 @@ lookup_fam_inst_env' -- The worker, local to this module lookup_fam_inst_env' match_fun _one_sided ie fam tys | isFamilyTyCon fam , Just (FamIE insts) <- lookupUFM ie fam - = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) - if arity < n_tys then -- Family type applications must be saturated - -- See Note [Over-saturated matches] - map wrap_extra_tys (find match_fun (take arity tys) insts) - else - find match_fun tys insts -- The common case - + = find match_fun tys insts -- The common case | otherwise = [] - where - arity = tyConArity fam - n_tys = length tys - extra_tys = drop arity tys - wrap_extra_tys fim@(FamInstMatch { fim_tys = match_tys }) - = fim { fim_tys = match_tys ++ extra_tys } - find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch] find _ _ [] = [] @@ -737,14 +747,20 @@ find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_branched = | instanceCantMatch rough_tcs mb_tcs = findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen' | otherwise - = case match_fun seen branch is_branched match_tys of + = case match_fun seen branch is_branched match_tys1 of (Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1) (Nothing, StopSearching) -> (Nothing, StopSearching) (Just subst, cont) -> (Just match, cont) where match = FamInstMatch { fim_instance = inst , fim_index = ind - , fim_tys = substTyVars subst tvs } + , fim_tys = substTyVars subst tvs `add_on` match_tys2} + where + -- Deal with over-saturation + -- See Note [Over-saturated matches] + (match_tys1, match_tys2) = splitAtList mb_tcs match_tys + add_on tys1 [] = tys1 -- The wildly common case + add_on tys1 tys2 = tys1 ++ tys2 lookup_fam_inst_env -- The worker, local to this module :: MatchFun @@ -851,7 +867,6 @@ topNormaliseType env ty normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type) normaliseTcApp env tc tys | isFamilyTyCon tc - , tyConArity tc <= length tys -- Unsaturated data families are possible , [FamInstMatch { fim_instance = fam_inst , fim_index = fam_ind , fim_tys = inst_tys }] <- lookupFamInstEnv env tc ntys |