Commit de32beff authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Do not create nested quantified constraints

Previously, we would accidentally make constraints like
forall a. C a => forall b. D b => E a b c as we traversed
superclasses. No longer!

This patch also expands Note [Eagerly expand given superclasses]
to work over quantified constraints; necessary for T16502b.

Close #17202 and #16502.

test cases: typecheck/should_compile/T{17202,16502{,b}}
parent 375b3c45
Pipeline #15646 passed with stages
in 438 minutes and 45 seconds
......@@ -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
......
......@@ -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
......
......@@ -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 }
......
......@@ -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
......
......@@ -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) }
......
......@@ -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
......
{-# 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))
{-# 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)
-}
......@@ -688,9 +688,10 @@ 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, [])
test('T12760', unless(compiler_debugged(), skip), compile, ['-O'])
......
{-# 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.
......@@ -551,6 +551,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, [''])
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