diff options
| -rw-r--r-- | compiler/basicTypes/Predicate.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/Constraint.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 114 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 14 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 20 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 2 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T16502b.hs | 35 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T17202.hs | 4 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 3 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T16502.hs | 31 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
11 files changed, 194 insertions, 36 deletions
diff --git a/compiler/basicTypes/Predicate.hs b/compiler/basicTypes/Predicate.hs index dab4e64..be9254d 100644 --- a/compiler/basicTypes/Predicate.hs +++ b/compiler/basicTypes/Predicate.hs @@ -50,7 +50,7 @@ data Pred = ClassPred Class [Type] | EqPred EqRel Type Type | IrredPred PredType - | ForAllPred [TyCoVarBinder] [PredType] PredType + | ForAllPred [TyVar] [PredType] PredType -- ForAllPred: see Note [Quantified constraints] in TcCanonical -- NB: There is no TuplePred case -- Tuple predicates like (Eq a, Ord b) are just treated @@ -67,7 +67,7 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of | Just clas <- tyConClass_maybe tc -> ClassPred clas tys - _ | (tvs, rho) <- splitForAllVarBndrs ev_ty + _ | (tvs, rho) <- splitForAllTys ev_ty , (theta, pred) <- splitFunTys rho , not (null tvs && null theta) -> ForAllPred tvs theta pred diff --git a/compiler/typecheck/Constraint.hs b/compiler/typecheck/Constraint.hs index 29a8700..459b457 100644 --- a/compiler/typecheck/Constraint.hs +++ b/compiler/typecheck/Constraint.hs @@ -764,7 +764,7 @@ isPendingScDict ct@(CDictCan { cc_pend_sc = True }) isPendingScDict _ = Nothing isPendingScInst :: QCInst -> Maybe QCInst --- Same as isPrendinScDict, but for QCInsts +-- Same as isPendingScDict, but for QCInsts isPendingScInst qci@(QCI { qci_pend_sc = True }) = Just (qci { qci_pend_sc = False }) isPendingScInst _ = Nothing diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index b1a0820..96f4b3f 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -96,8 +96,8 @@ canonicalize (CNonCanonical { cc_ev = ev }) canEqNC ev eq_rel ty1 ty2 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred) canIrred ev - ForAllPred _ _ pred -> do traceTcS "canEvNC:forall" (ppr pred) - canForAll ev (isClassPred pred) + ForAllPred tvs theta p -> do traceTcS "canEvNC:forall" (ppr pred) + canForAllNC ev tvs theta p where pred = ctEvPred ev @@ -373,6 +373,10 @@ So we may need to do a little work on the givens to expose the class that has the superclasses. That's why the superclass expansion for Givens happens in canClassNC. +This same scenario happens with quantified constraints, whose superclasses +are also eagerly expanded. Test case: typecheck/should_compile/T16502b +These are handled in canForAllNC, analogously to canClassNC. + Note [Why adding superclasses can help] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Examples of how adding superclasses can help: @@ -438,6 +442,46 @@ happen. Mind you, now that Wanteds cannot rewrite Derived, I think this particular situation can't happen. + +Note [Nested quantified constraint superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (typecheck/should_compile/T17202) + + class C1 a + class (forall c. C1 c) => C2 a + class (forall b. (b ~ F a) => C2 a) => C3 a + +Elsewhere in the code, we get a [G] g1 :: C3 a. We expand its superclass +to get [G] g2 :: (forall b. (b ~ F a) => C2 a). This constraint has a +superclass, as well. But we now must be careful: we cannot just add +(forall c. C1 c) as a Given, because we need to remember g2's context. +That new constraint is Given only when forall b. (b ~ F a) is true. + +It's tempting to make the new Given be (forall b. (b ~ F a) => forall c. C1 c), +but that's problematic, because it's nested, and ForAllPred is not capable +of representing a nested quantified constraint. (We could change ForAllPred +to allow this, but the solution in this Note is much more local and simpler.) + +So, we swizzle it around to get (forall b c. (b ~ F a) => C1 c). + +More generally, if we are expanding the superclasses of + g0 :: forall tvs. theta => cls tys +and find a superclass constraint + forall sc_tvs. sc_theta => sc_inner_pred +we must have a selector + sel_id :: forall cls_tvs. cls cls_tvs -> forall sc_tvs. sc_theta => sc_inner_pred +and thus build + g_sc :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred + g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. \ sc_theta_ids. + sel_id tys (g0 tvs theta_ids) sc_tvs sc_theta_ids + +Actually, we cheat a bit by eta-reducing: note that sc_theta_ids are both the +last bound variables and the last arguments. This avoids the need to produce +the sc_theta_ids at all. So our final construction is + + g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. + sel_id tys (g0 tvs theta_ids) sc_tvs + -} makeSuperClasses :: [Ct] -> TcS [Ct] @@ -483,31 +527,49 @@ mk_strict_superclasses :: NameSet -> CtEvidence -- Always return the immediate superclasses of (cls tys); -- and expand their superclasses, provided none of them are in rec_clss -- nor are repeated -mk_strict_superclasses rec_clss ev tvs theta cls tys - | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev - = concatMapM (do_one_given evar (mk_given_loc loc)) $ +mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) + tvs theta cls tys + = concatMapM (do_one_given (mk_given_loc loc)) $ classSCSelIds cls where dict_ids = mkTemplateLocals theta size = sizeTypes tys - do_one_given evar given_loc sel_id + do_one_given given_loc sel_id | isUnliftedType sc_pred , not (null tvs && null theta) = -- See Note [Equality superclasses in quantified constraints] return [] | otherwise = do { given_ev <- newGivenEvVar given_loc $ - (given_ty, mk_sc_sel evar sel_id) + mk_given_desc sel_id sc_pred ; mk_superclasses rec_clss given_ev tvs theta sc_pred } where sc_pred = funResultTy (piResultTys (idType sel_id) tys) - given_ty = mkInfSigmaTy tvs theta sc_pred - mk_sc_sel evar sel_id - = EvExpr $ mkLams tvs $ mkLams dict_ids $ - Var sel_id `mkTyApps` tys `App` - (evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids) + -- See Note [Nested quantified constraint superclasses] + mk_given_desc :: Id -> PredType -> (PredType, EvTerm) + mk_given_desc sel_id sc_pred + = (swizzled_pred, swizzled_evterm) + where + (sc_tvs, sc_rho) = splitForAllTys sc_pred + (sc_theta, sc_inner_pred) = splitFunTys sc_rho + + all_tvs = tvs `chkAppend` sc_tvs + all_theta = theta `chkAppend` sc_theta + swizzled_pred = mkInfSigmaTy all_tvs all_theta sc_inner_pred + + -- evar :: forall tvs. theta => cls tys + -- sel_id :: forall cls_tvs. cls cls_tvs + -- -> forall sc_tvs. sc_theta => sc_inner_pred + -- swizzled_evterm :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred + swizzled_evterm = EvExpr $ + mkLams all_tvs $ + mkLams dict_ids $ + Var sel_id + `mkTyApps` tys + `App` (evId evar `mkVarApps` (tvs ++ dict_ids)) + `mkVarApps` sc_tvs mk_given_loc loc | isCTupleClass cls @@ -743,9 +805,23 @@ Note that a quantified constraint is never /inferred/ quantified constraint in its type if it is given an explicit type signature. -Note that we implement -} +canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType + -> TcS (StopOrContinue Ct) +canForAllNC ev tvs theta pred + | isGiven ev -- See Note [Eagerly expand given superclasses] + , Just (cls, tys) <- cls_pred_tys_maybe + = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys + ; emitWork sc_cts + ; canForAll ev False } + + | otherwise + = canForAll ev (isJust cls_pred_tys_maybe) + + where + cls_pred_tys_maybe = getClassPredTys_maybe pred + canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) -- We have a constraint (forall as. blah => C tys) canForAll ev pend_sc @@ -760,14 +836,14 @@ canForAll ev pend_sc do { -- Now decompose into its pieces and solve it -- (It takes a lot less code to flatten before decomposing.) ; case classifyPredType (ctEvPred new_ev) of - ForAllPred tv_bndrs theta pred - -> solveForAll new_ev tv_bndrs theta pred pend_sc + ForAllPred tvs theta pred + -> solveForAll new_ev tvs theta pred pend_sc _ -> pprPanic "canForAll" (ppr new_ev) } } -solveForAll :: CtEvidence -> [TyVarBinder] -> TcThetaType -> PredType -> Bool +solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool -> TcS (StopOrContinue Ct) -solveForAll ev tv_bndrs theta pred pend_sc +solveForAll ev tvs theta pred pend_sc | CtWanted { ctev_dest = dest } <- ev = -- See Note [Solving a Wanted forall-constraint] do { let skol_info = QuantCtxtSkol @@ -794,10 +870,10 @@ solveForAll ev tv_bndrs theta pred pend_sc ; stopWith ev "Given forall-constraint" } | otherwise - = stopWith ev "Derived forall-constraint" + = do { traceTcS "discarding derived forall-constraint" (ppr ev) + ; stopWith ev "Derived forall-constraint" } where loc = ctEvLoc ev - tvs = binderVars tv_bndrs qci = QCI { qci_ev = ev, qci_tvs = tvs , qci_pred = pred, qci_pend_sc = pend_sc } diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 2a77c62..43ec10f 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -2655,15 +2655,19 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult matchLocalInst pred loc = do { ics <- getInertCans ; case match_local_inst (inert_insts ics) of - ([], False) -> return NoInstance + ([], False) -> do { traceTcS "No local instance for" (ppr pred) + ; return NoInstance } ([(dfun_ev, inst_tys)], unifs) | not unifs -> do { let dfun_id = ctEvEvId dfun_ev ; (tys, theta) <- instDFunType dfun_id inst_tys - ; return $ OneInst { cir_new_theta = theta - , cir_mk_ev = evDFunApp dfun_id tys - , cir_what = LocalInstance } } - _ -> return NotSure } + ; let result = OneInst { cir_new_theta = theta + , cir_mk_ev = evDFunApp dfun_id tys + , cir_what = LocalInstance } + ; traceTcS "Local inst found:" (ppr result) + ; return result } + _ -> do { traceTcS "Multiple local instances for" (ppr pred) + ; return NotSure }} where pred_tv_set = tyCoVarsOfType pred diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index aa5b283..87ff629 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -1530,13 +1530,20 @@ lookupInertTyVar ieqs tv addInertForAll :: QCInst -> TcS () -- Add a local Given instance, typically arising from a type signature addInertForAll new_qci - = updInertCans $ \ics -> - ics { inert_insts = add_qci (inert_insts ics) } + = do { ics <- getInertCans + ; insts' <- add_qci (inert_insts ics) + ; setInertCans (ics { inert_insts = insts' }) } where - add_qci :: [QCInst] -> [QCInst] + add_qci :: [QCInst] -> TcS [QCInst] -- See Note [Do not add duplicate quantified instances] - add_qci qcis | any same_qci qcis = qcis - | otherwise = new_qci : qcis + add_qci qcis + | any same_qci qcis + = do { traceTcS "skipping duplicate quantified instance" (ppr new_qci) + ; return qcis } + + | otherwise + = do { traceTcS "adding new inert quantified instance" (ppr new_qci) + ; return (new_qci : qcis) } same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci)) (ctEvPred (qci_ev new_qci)) @@ -1557,7 +1564,7 @@ because of that. But without doing duplicate-elimination we will have two matching QCInsts when we try to solve constraints arising from f's RHS. -The simplest thing is simply to eliminate duplicattes, which we do here. +The simplest thing is simply to eliminate duplicates, which we do here. -} {- ********************************************************************* @@ -3023,6 +3030,7 @@ emitWorkNC evs = emitWork (map mkNonCanonical evs) emitWork :: [Ct] -> TcS () +emitWork [] = return () -- avoid printing, among other work emitWork cts = do { traceTcS "Emitting fresh work" (vcat (map ppr cts)) ; updWorkListTcS (extendWorkListCts cts) } diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index a4074af..0321dad 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1931,7 +1931,7 @@ checkInstTermination theta head_pred -- See Note [Invisible arguments and termination] ForAllPred tvs _ head_pred' - -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred' + -> check (foralld_tvs `extendVarSetList` tvs) head_pred' -- Termination of the quantified predicate itself is checked -- when the predicates are individually checked for validity diff --git a/testsuite/tests/typecheck/should_compile/T16502b.hs b/testsuite/tests/typecheck/should_compile/T16502b.hs new file mode 100644 index 0000000..03855c4 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T16502b.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module T16502b where + +import Data.Kind + +type family Sing :: k -> Type + +class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) + => ShowSing' (z :: k) +instance Show (Sing z) => ShowSing' (z :: k) + +class (forall (z :: k). ShowSing' z) => ShowSing k +instance (forall (z :: k). ShowSing' z) => ShowSing k + +newtype Foo a = MkFoo a +data SFoo :: forall a. Foo a -> Type where + SMkFoo :: Sing x -> SFoo (MkFoo x) +type instance Sing = SFoo +deriving instance ShowSing a => Show (SFoo (z :: Foo a)) + +newtype Bar a = MkBar (Foo a) +data SBar :: forall a. Bar a -> Type where + SMkBar :: forall a (x :: Foo a). Sing x -> SBar (MkBar x) +type instance Sing = SBar +deriving instance ShowSing (Foo a) => Show (SBar (z :: Bar a)) diff --git a/testsuite/tests/typecheck/should_compile/T17202.hs b/testsuite/tests/typecheck/should_compile/T17202.hs index d9d6ec2..9f28ccc 100644 --- a/testsuite/tests/typecheck/should_compile/T17202.hs +++ b/testsuite/tests/typecheck/should_compile/T17202.hs @@ -1,6 +1,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds #-} module T17202 where @@ -15,6 +16,7 @@ data Dict c = c => Dict foo :: forall a. C3 a => Dict (C1 a) foo = Dict +{- is rejected due to #17719 bar :: forall a. C3 a => Dict (C1 a) bar = Dict :: C2 a => Dict (C1 a) - +-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 0f61b57..cedcb37 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -688,8 +688,9 @@ test('T16832', normal, ghci_script, ['T16832.script']) test('T16995', normal, compile, ['']) test('T17007', normal, compile, ['']) test('T17067', normal, compile, ['']) -test('T17202', expect_broken(17202), compile, ['']) +test('T17202', normal, compile, ['']) test('T15839a', normal, compile, ['']) test('T15839b', normal, compile, ['']) +test('T16502b', normal, compile, ['']) test('T17343', exit_code(1), compile_and_run, ['']) test('T17566', [extra_files(['T17566a.hs'])], makefile_test, []) diff --git a/testsuite/tests/typecheck/should_fail/T16502.hs b/testsuite/tests/typecheck/should_fail/T16502.hs new file mode 100644 index 0000000..5fac062 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16502.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE InstanceSigs #-} +module T16502 where + +import Data.Kind + +class (forall c. c ~ T a => Show (c b)) => ShowT a b +instance Show (T a b) => ShowT a b + +class (forall b. Show b => ShowT a b) => C a where + type family T a :: Type -> Type + +data D a = MkD (T a Int) + +instance C a => Show (D a) where + showsPrec p (MkD x) + = (showParen (p > 10) $ showString "MkD " . showsPrec 11 x) + +-- This is rejected because we cannot derive (Show (D a)) from (C a) +-- due to troublesome quantified constraints. And then the error +-- message mentions the internal name of the default method for show. +-- Simon thinks that we should accept the fact that this doesn't get +-- accepted, given that a quantified constraint for (Show (c b)) is far +-- too applicable to be useful. So we're left with the suboptimal +-- error message. diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 156042c..ad1beec 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -550,6 +550,7 @@ test('T17355', normal, compile_fail, ['']) test('T17360', normal, compile_fail, ['']) test('T17563', normal, compile_fail, ['']) test('T16946', normal, compile_fail, ['']) +test('T16502', expect_broken(12854), compile, ['']) test('T17566b', normal, compile_fail, ['']) test('T17566c', normal, compile_fail, ['']) test('T17773', normal, compile_fail, ['']) |