Commit 0dc86f6b authored by Matthías Páll Gissurarson's avatar Matthías Páll Gissurarson Committed by Krzysztof Gogolewski

Clone relevant constraints to avoid side-effects on HoleDests. Fixes #15370.

Summary: When looking for valid hole fits, the constraints relevant
to the hole may sometimes contain a HoleDest. Previously,
these were not cloned, which could cause the filling of filled
coercion hole being, which would cause an assert to fail. This is now fixed.

Test Plan: Regression test included.

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15370

Differential Revision: https://phabricator.haskell.org/D5004
parent 47561c91
......@@ -950,16 +950,21 @@ tcCheckHoleFit relevantCts implics hole_ty ty = discardErrs $
tcSubType_NC ExprSigCtxt ty hole_ty
; traceTc "Checking hole fit {" empty
; traceTc "wanteds are: " $ ppr wanted
-- We add the relevantCts to the wanteds generated by the call to
-- tcSubType_NC, see Note [Relevant Constraints]
; let w_rel_cts = addSimples wanted relevantCts
; if isEmptyWC w_rel_cts
; if isEmptyWC wanted && isEmptyBag relevantCts
then traceTc "}" empty >> return (True, wrp)
else do { fresh_binds <- newTcEvBinds
-- The relevant constraints may contain HoleDests, so we must
-- take care to clone them as well (to avoid #15370).
; cloned_relevants <- mapBagM cloneSimple relevantCts
-- We wrap the WC in the nested implications, see
-- Note [Nested Implications]
; let outermost_first = reverse implics
setWC = setWCAndBinds fresh_binds
-- We add the cloned relevants to the wanteds generated by
-- the call to tcSubType_NC, see Note [Relevant Constraints]
-- There's no need to clone the wanteds, because they are
-- freshly generated by `tcSubtype_NC`.
w_rel_cts = addSimples wanted cloned_relevants
w_givens = foldr setWC w_rel_cts outermost_first
; traceTc "w_givens are: " $ ppr w_givens
; rem <- runTcSDeriveds $ simpl_top w_givens
......
......@@ -39,7 +39,7 @@ module TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
newWanted, newWanteds, cloneWanted, cloneWC,
newWanted, newWanteds, cloneWanted, cloneSimple, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
......@@ -188,14 +188,15 @@ cloneWanted ct
where
ev = ctEvidence ct
cloneSimple :: Ct -> TcM Ct
cloneSimple = fmap mkNonCanonical . cloneWanted
cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
= do { simples' <- mapBagM clone_one simples
= do { simples' <- mapBagM cloneSimple simples
; implics' <- mapBagM clone_implic implics
; return (wc { wc_simple = simples', wc_impl = implics' }) }
where
clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }
clone_implic implic@(Implic { ic_wanted = inner_wanted })
= do { inner_wanted' <- cloneWC inner_wanted
; return (implic { ic_wanted = inner_wanted' }) }
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
data S (a :: Either x y)
mkRefl :: n :~: j
mkRefl = Refl
right :: forall (r :: Either x y).
S r -> ()
right no =
case mkRefl @x @y of
Refl -> no + _
T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘n’ with ‘j’
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k (n :: k) (j :: k). n :~: j
at T15370.hs:13:1-17
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k (n :: k) (j :: k). n :~: j
at T15370.hs:13:1-17
Expected type: n :~: j
Actual type: n :~: n
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at T15370.hs:14:1)
T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘S r’ with ‘()’
Expected type: ()
Actual type: S r
• In the expression: no + _
In a case alternative: Refl -> no + _
In the expression: case mkRefl @x @y of { Refl -> no + _ }
• Relevant bindings include
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: S r
Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
the type signature for:
right :: forall x y (r :: Either x y). S r -> ()
at T15370.hs:(16,1)-(17,18)
• In the second argument of ‘(+)’, namely ‘_’
In the expression: no + _
In a case alternative: Refl -> no + _
• Relevant bindings include
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
Constraints include y ~ x (from T15370.hs:20:5-8)
......@@ -398,6 +398,7 @@ test('abstract_refinement_hole_fits', normal, compile, ['-fdefer-type-errors -fn
test('free_monad_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -fno-max-refinement-hole-fits -frefinement-level-hole-fits=2 -funclutter-valid-hole-fits'])
test('constraint_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -fno-max-refinement-hole-fits -frefinement-level-hole-fits=2 -funclutter-valid-hole-fits'])
test('type_in_type_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits'])
test('T15370', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -funclutter-valid-hole-fits'])
test('T7408', normal, compile, [''])
test('UnboxStrictPrimitiveFields', normal, compile, [''])
test('T7541', normal, compile, [''])
......
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