[Git][ghc/ghc][wip/T23070-unify] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Apr 10 22:43:35 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
c7ebcaba by Simon Peyton Jones at 2023-04-10T23:45:05+01:00
More wibbles
- - - - -
11 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Interact.hs
- libraries/base/GHC/Bits.hs
- testsuite/tests/impredicative/icfp20-fail.stderr
- testsuite/tests/indexed-types/should_fail/T4179.stderr
- testsuite/tests/indexed-types/should_fail/T4254b.hs
- − testsuite/tests/indexed-types/should_fail/T4254b.stderr
- testsuite/tests/indexed-types/should_fail/T9662.stderr
- testsuite/tests/indexed-types/should_fail/all.T
- testsuite/tests/partial-sigs/should_fail/T14584a.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -16,6 +16,7 @@ import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
+import GHC.Tc.Solver.Types
import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey )
@@ -31,6 +32,7 @@ import GHC.Types.SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Unique( hasKey )
+import GHC.Utils.Monad ( foldlM )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
@@ -69,24 +71,33 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
; addSolvedDict what ev cls xis
; chooseInstance work_item lkup_res }
_ -> -- NoInstance or NotSure
- -- We didn't solve it; so try functional dependencies with
- -- the instance environment
- do { improved <- doTopFundepImprovement work_item
- ; if improved
- then startAgainWith work_item
- else tryLastResortProhibitedSuperclass inerts work_item } }
+ -- We didn't solve it; so try functional dependencies
+ tryFunDeps work_item }
where
dict_loc = ctEvLoc ev
-
doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
--- | As a last resort, we TEMPORARILY allow a prohibited superclass solve,
+tryFunDeps :: Ct -> TcS (StopOrContinue Ct)
+-- Try functional dependencies
+-- We do local improvement, then try top level; and we do all this last
+-- See Note [Do fundeps last]
+tryFunDeps work_item
+ = do { improved <- doLocalFunDepImprovement work_item
+ ; if improved then startAgainWith work_item else
+
+ do { improved <- doTopFunDepImprovement work_item
+ ; if improved then startAgainWith work_item else
+
+ do { inerts <- getTcSInerts
+ ; tryLastResortProhibitedSuperclass inerts work_item } } }
+
+tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct)
+-- ^ As a last resort, we TEMPORARILY allow a prohibited superclass solve,
-- emitting a loud warning when doing so: we might be creating non-terminating
-- evidence (as we are in T22912 for example).
--
-- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance.
-tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct)
tryLastResortProhibitedSuperclass inerts
work_item@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = xis })
| let loc_w = ctEvLoc ev_w
@@ -681,7 +692,7 @@ This Note describes a delicate interaction that constrains the orientation of
equalities. This one is about fundeps, but the /exact/ same thing arises for
type-family injectivity constraints: see Note [Improvement orientation].
-doTopFundepImprovement compares the constraint with all the instance
+doTopFunDepImprovement compares the constraint with all the instance
declarations, to see if we can produce any equalities. E.g
class C2 a b | a -> b
instance C Int Bool
@@ -695,7 +706,7 @@ There is a nasty corner in #19415 which led to the typechecker looping:
work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char
where kb0, b0 are unification vars
- ==> {doTopFundepImprovement: compare work_item with instance,
+ ==> {doTopFunDepImprovement: compare work_item with instance,
generate /fresh/ unification variables kfresh0, yfresh0,
emit a new Wanted, and add dwrk to inert set}
@@ -811,6 +822,29 @@ wanteds. This solution was not complete, and caused a failures while trying
to solve for transitive functional dependencies (test case: T21703)
-- End of Historical note: Failed Alternative Plan (3) --
+Note [Do fundeps last]
+~~~~~~~~~~~~~~~~~~~~~~
+Consider T4254b:
+ class FD a b | a -> b where { op :: a -> b }
+
+ instance FD Int Bool
+
+ foo :: forall a b. (a~Int,FD a b) => a -> Bool
+ foo = op
+
+From the ambiguity check on the type signature we get
+ [G] FD Int b
+ [W] FD Int beta
+Interacting these gives beta:=b; then we start again and solve without
+trying fundeps between the new [W] FD Int b and the top-level instance.
+If we did, we'd generate [W] b ~ Bool, which fails.
+
+From the definition `foo = op` we get
+ [G] FD Int b
+ [W] FD Int Bool
+We solve this from the top level instance before even trying fundeps.
+If we did try fundeps, we'd generate [W] b ~ Bool, which fails.
+
Note [Weird fundeps]
~~~~~~~~~~~~~~~~~~~~
Consider class Het a b | a -> b where
@@ -833,13 +867,60 @@ as the fundeps.
#7875 is a case in point.
-}
-doTopFundepImprovement :: Ct -> TcS Bool
+doLocalFunDepImprovement :: Ct -> TcS Bool
+-- Add wanted constraints from type-class functional dependencies.
+doLocalFunDepImprovement (CDictCan { cc_ev = work_ev, cc_class = cls })
+ = do { inerts <- getInertCans
+ ; foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) }
+ -- No need to check flavour; fundeps work between
+ -- any pair of constraints, regardless of flavour
+ -- Importantly we don't throw workitem back in the
+ -- worklist because this can cause loops (see #5236)
+ where
+ work_pred = ctEvPred work_ev
+ work_loc = ctEvLoc work_ev
+
+ add_fds :: Bool -> Ct -> TcS Bool
+ add_fds so_far inert_ct
+ | isGiven work_ev && isGiven inert_ev
+ -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps]
+ = return so_far
+ | otherwise
+ = do { traceTcS "doLocalFunDepImprovement" (vcat
+ [ ppr work_ev
+ , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
+ , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
+ , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ])
+
+ ; unifs <- emitFunDepWanteds work_ev $
+ improveFromAnother (derived_loc, inert_rewriters)
+ inert_pred work_pred
+ -- We don't really rewrite tys2, see below
+ -- _rewritten_tys2, so that's ok
+ ; return (so_far || unifs)
+ }
+ where
+ inert_ev = ctEvidence inert_ct
+ inert_pred = ctEvPred inert_ev
+ inert_loc = ctEvLoc inert_ev
+ inert_rewriters = ctRewriters inert_ct
+ derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
+ ctl_depth inert_loc
+ , ctl_origin = FunDepOrigin1 work_pred
+ (ctLocOrigin work_loc)
+ (ctLocSpan work_loc)
+ inert_pred
+ (ctLocOrigin inert_loc)
+ (ctLocSpan inert_loc) }
+
+doLocalFunDepImprovement work_item = pprPanic "doLocalFunDepImprovement" (ppr work_item)
+
+doTopFunDepImprovement :: Ct -> TcS Bool
-- Try to functional-dependency improvement between the constraint
-- and the top-level instance declarations
-- See Note [Fundeps with instances, and equality orientation]
-- See also Note [Weird fundeps]
-doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
- , cc_tyargs = xis })
+doTopFunDepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = xis })
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
@@ -857,5 +938,4 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
inst_pred inst_loc }
, emptyRewriterSet )
-doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_item)
-
+doTopFunDepImprovement work_item = pprPanic "doTopFunDepImprovement" (ppr work_item)
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1489,11 +1489,12 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
rewriters = rewriterSetFromCo kind_co
; traceTcS "Hetero equality gives rise to kind equality"
- (ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
+ (ppr swapped $$
+ ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co
- ; canEqCanLHSHomo type_ev eq_rel swapped lhs1 ps_xi1 new_xi2 new_xi2 }}
+ ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }}
where
mk_kind_eq :: TcS (CoercionN, Bool)
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -11,7 +11,6 @@ import GHC.Tc.Solver.Canonical
import GHC.Tc.Solver.Dict
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
-import GHC.Tc.Instance.FunDeps
import GHC.Tc.Instance.Class ( safeOverlap )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types
@@ -22,7 +21,6 @@ import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Core.InstEnv ( Coherence(..) )
-import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.Coercion
@@ -1028,10 +1026,7 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t
= interactGivenIP inerts ct_w
| otherwise
- = do { unif_happened <- addFunDepWork inerts ev_w cls
- ; if unif_happened
- then startAgainWith ct_w
- else continueWith ct_w }
+ = continueWith ct_w
interactDict _ wi = pprPanic "interactDict" (ppr wi)
@@ -1136,50 +1131,6 @@ shortCutSolver dflags ev_w ev_i
Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
| otherwise = mzero
-addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS Bool
--- Add wanted constraints from type-class functional dependencies.
-addFunDepWork inerts work_ev cls
- = foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls)
- -- No need to check flavour; fundeps work between
- -- any pair of constraints, regardless of flavour
- -- Importantly we don't throw workitem back in the
- -- worklist because this can cause loops (see #5236)
- where
- work_pred = ctEvPred work_ev
- work_loc = ctEvLoc work_ev
-
- add_fds :: Bool -> Ct -> TcS Bool
- add_fds so_far inert_ct
- | isGiven work_ev && isGiven inert_ev
- -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps]
- = return so_far
- | otherwise
- = do { traceTcS "addFunDepWork" (vcat
- [ ppr work_ev
- , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
- , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
- , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ])
-
- ; unifs <- emitFunDepWanteds work_ev $
- improveFromAnother (derived_loc, inert_rewriters)
- inert_pred work_pred
- -- We don't really rewrite tys2, see below
- -- _rewritten_tys2, so that's ok
- ; return (so_far || unifs)
- }
- where
- inert_ev = ctEvidence inert_ct
- inert_pred = ctEvPred inert_ev
- inert_loc = ctEvLoc inert_ev
- inert_rewriters = ctRewriters inert_ct
- derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
- ctl_depth inert_loc
- , ctl_origin = FunDepOrigin1 work_pred
- (ctLocOrigin work_loc)
- (ctLocSpan work_loc)
- inert_pred
- (ctLocOrigin inert_loc)
- (ctLocSpan inert_loc) }
{-
**********************************************************************
=====================================
libraries/base/GHC/Bits.hs
=====================================
@@ -722,3 +722,4 @@ own to enable constant folding; for example 'shift':
-- > ; True -> Just (W16# (narrow16Word# (int2Word# b1)))
-- > }
-- > }
+x=y
\ No newline at end of file
=====================================
testsuite/tests/impredicative/icfp20-fail.stderr
=====================================
@@ -1,7 +1,6 @@
icfp20-fail.hs:20:10: error: [GHC-83865]
- • Couldn't match type: forall a. a -> a
- with: b -> b
+ • Couldn't match type ‘SId’ with ‘b -> b’
Expected: SId -> b -> b
Actual: SId -> SId
• In the expression: id
=====================================
testsuite/tests/indexed-types/should_fail/T4179.stderr
=====================================
@@ -1,13 +1,13 @@
T4179.hs:26:16: error: [GHC-83865]
- • Couldn't match type: A3 (x (A2 (FCon x) -> A3 (FCon x)))
- with: A3 (FCon x)
+ • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
+ with: A2 (FCon x)
Expected: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (FCon x) -> A3 (FCon x)
Actual: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
- NB: ‘A3’ is a non-injective type family
+ NB: ‘A2’ is a non-injective type family
• In the first argument of ‘foldDoC’, namely ‘op’
In the expression: foldDoC op
In an equation for ‘fCon’: fCon = foldDoC op
=====================================
testsuite/tests/indexed-types/should_fail/T4254b.hs
=====================================
@@ -11,3 +11,22 @@ fails :: forall a b. (a~Int,FD a b) => a -> Bool
fails = op
-- Could fail: no proof that b~Bool
-- But can also succeed; it's not a *wanted* constraint
+
+{- Interestingly, the ambiguity check for the type sig succeeds:
+
+[G] FD Int b
+[W] FD Int beta
+
+We get [W] beta~b; we unify immediately, and then solve.
+All before we interact the [W] FD Int beta with the
+top-level instances (which would give rise to [W] beta~Bool).
+
+One the other hand, from `fails = op` we get
+
+[G] FD Int b
+[W] FD Int Bool
+
+Interacting those two gives [W] b~Bool; bu this doesn't
+happen becase we now solve first.
+
+-}
\ No newline at end of file
=====================================
testsuite/tests/indexed-types/should_fail/T4254b.stderr deleted
=====================================
@@ -1,20 +0,0 @@
-
-T4254b.hs:10:10: error: [GHC-25897]
- • Couldn't match type ‘b’ with ‘Bool’
- arising from a functional dependency between constraints:
- ‘FD Int Bool’
- arising from a type ambiguity check for
- the type signature for ‘fails’ at T4254b.hs:10:10-48
- ‘FD Int b’
- arising from the type signature for:
- fails :: forall a b.
- (a ~ Int, FD a b) =>
- a -> Bool at T4254b.hs:10:10-48
- ‘b’ is a rigid type variable bound by
- the type signature for:
- fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
- at T4254b.hs:10:10-48
- • In the ambiguity check for ‘fails’
- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
- In the type signature:
- fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
=====================================
testsuite/tests/indexed-types/should_fail/T9662.stderr
=====================================
@@ -1,13 +1,13 @@
T9662.hs:49:8: error: [GHC-25897]
- • Couldn't match type ‘n’ with ‘Int’
+ • Couldn't match type ‘k’ with ‘Int’
Expected: Exp (((sh :. k) :. m) :. n)
-> Exp (((sh :. m) :. n) :. k)
Actual: Exp
(Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-> Exp
(Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
- ‘n’ is a rigid type variable bound by
+ ‘k’ is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
=====================================
testsuite/tests/indexed-types/should_fail/all.T
=====================================
@@ -58,7 +58,7 @@ test('T3330a', normal, compile_fail, [''])
test('T3330b', normal, compile_fail, [''])
test('T3330c', normal, compile_fail, [''])
test('T4179', normal, compile_fail, [''])
-test('T4254b', normal, compile_fail, [''])
+test('T4254b', normal, compile, [''])
test('T2239', normal, compile, [''])
test('T3440', expect_broken(19974), compile_fail, [''])
test('T4485', normal, compile_fail, [''])
=====================================
testsuite/tests/partial-sigs/should_fail/T14584a.stderr
=====================================
@@ -32,3 +32,11 @@ T14584a.hs:15:17: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
In the expression: id @m
In an equation for ‘h’: h = id @m
• Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
+
+T14584a.hs:16:8: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
+ • Couldn't match expected type ‘()’ with actual type ‘m -> m’
+ • Probable cause: ‘h’ is applied to too few arguments
+ In the expression: h
+ In the expression: let h = id @m in h
+ In an equation for ‘g’: g = let h = id @m in h
+ • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c7ebcabad4bb86aad3ffafb38d43b3d2c449ff4d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c7ebcabad4bb86aad3ffafb38d43b3d2c449ff4d
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230410/8c765a20/attachment-0001.html>
More information about the ghc-commits
mailing list