[commit: ghc] master: Clone relevant constraints to avoid side-effects on HoleDests. Fixes #15370. (0dc86f6)
git at git.haskell.org
git at git.haskell.org
Tue Jul 24 21:59:33 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/0dc86f6bc454253969dedc31bed477eded4cf82d/ghc
>---------------------------------------------------------------
commit 0dc86f6bc454253969dedc31bed477eded4cf82d
Author: Matthías Páll Gissurarson <mpg at mpg.is>
Date: Tue Jul 24 23:57:48 2018 +0200
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
>---------------------------------------------------------------
0dc86f6bc454253969dedc31bed477eded4cf82d
compiler/typecheck/TcHoleErrors.hs | 13 ++++---
compiler/typecheck/TcMType.hs | 9 ++---
testsuite/tests/typecheck/should_compile/T15370.hs | 20 +++++++++++
.../tests/typecheck/should_compile/T15370.stderr | 42 ++++++++++++++++++++++
testsuite/tests/typecheck/should_compile/all.T | 1 +
5 files changed, 77 insertions(+), 8 deletions(-)
diff --git a/compiler/typecheck/TcHoleErrors.hs b/compiler/typecheck/TcHoleErrors.hs
index 173abbd..7dde74f 100644
--- a/compiler/typecheck/TcHoleErrors.hs
+++ b/compiler/typecheck/TcHoleErrors.hs
@@ -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
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 8a96cb0..6e348d8 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -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' }) }
diff --git a/testsuite/tests/typecheck/should_compile/T15370.hs b/testsuite/tests/typecheck/should_compile/T15370.hs
new file mode 100644
index 0000000..acccf03
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15370.hs
@@ -0,0 +1,20 @@
+{-# 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 + _
diff --git a/testsuite/tests/typecheck/should_compile/T15370.stderr b/testsuite/tests/typecheck/should_compile/T15370.stderr
new file mode 100644
index 0000000..f26cf92
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15370.stderr
@@ -0,0 +1,42 @@
+
+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)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9d5d7c1..053f949 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -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, [''])
More information about the ghc-commits
mailing list