Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC
Commits:
-
44e59c0a
by Simon Peyton Jones at 2025-09-07T23:55:37+01:00
7 changed files:
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Equality.hs
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail10.stderr
- testsuite/tests/parser/should_fail/RecordDotSyntaxFail13.stderr
- testsuite/tests/polykinds/T6068.stdout
- testsuite/tests/typecheck/should_compile/T13651.hs
- testsuite/tests/typecheck/should_fail/T19415.stderr
Changes:
| ... | ... | @@ -468,53 +468,29 @@ defaultEquality ct |
| 468 | 468 | z_ty1 <- TcS.zonkTcType ty1
|
| 469 | 469 | ; z_ty2 <- TcS.zonkTcType ty2
|
| 470 | 470 | ; case eq_rel of
|
| 471 | - { NomEq ->
|
|
| 472 | - -- Now see if either LHS or RHS is a bare type variable
|
|
| 473 | - -- You might think the type variable will only be on the LHS
|
|
| 474 | - -- but with a type function we might get F t1 ~ alpha
|
|
| 475 | - case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
|
|
| 476 | - (Just z_tv1, _) -> try_default_tv z_tv1 z_ty2
|
|
| 477 | - (_, Just z_tv2) -> try_default_tv z_tv2 z_ty1
|
|
| 478 | - _ -> return False ;
|
|
| 479 | - |
|
| 480 | - ; ReprEq
|
|
| 481 | - -- See Note [Defaulting representational equalities]
|
|
| 482 | - | CIrredCan (IrredCt { ir_reason }) <- ct
|
|
| 483 | - , isInsolubleReason ir_reason
|
|
| 484 | - -- Don't do this for definitely insoluble representational
|
|
| 485 | - -- equalities such as Int ~R# Bool.
|
|
| 486 | - -> return False
|
|
| 487 | - | otherwise
|
|
| 488 | - ->
|
|
| 489 | - do { traceTcS "defaultEquality ReprEq {" $ vcat
|
|
| 490 | - [ text "ct:" <+> ppr ct
|
|
| 491 | - , text "z_ty1:" <+> ppr z_ty1
|
|
| 492 | - , text "z_ty2:" <+> ppr z_ty2
|
|
| 493 | - ]
|
|
| 494 | - -- Promote this representational equality to a nominal equality.
|
|
| 495 | - --
|
|
| 496 | - -- This handles cases such as @IO alpha[tau] ~R# IO Int@
|
|
| 497 | - -- by defaulting @alpha := Int@, which is useful in practice
|
|
| 498 | - -- (see Note [Defaulting representational equalities]).
|
|
| 499 | - ; (co, new_eqs, _unifs) <-
|
|
| 500 | - wrapUnifierX (ctEvidence ct) Nominal $
|
|
| 501 | - -- NB: nominal equality!
|
|
| 502 | - \ uenv -> uType uenv z_ty1 z_ty2
|
|
| 503 | - -- Only accept this solution if no new equalities are produced
|
|
| 504 | - -- by the unifier.
|
|
| 505 | - --
|
|
| 506 | - -- See Note [Defaulting representational equalities].
|
|
| 507 | - ; if null new_eqs
|
|
| 508 | - then do { setEvBindIfWanted (ctEvidence ct) EvCanonical $
|
|
| 509 | - (evCoercion $ mkSubCo co)
|
|
| 510 | - ; return True }
|
|
| 511 | - else return False
|
|
| 512 | - } } }
|
|
| 471 | + NomEq -> -- Now see if either LHS or RHS is a bare type variable
|
|
| 472 | + -- You might think the type variable will only be on the LHS
|
|
| 473 | + -- but with a type function we might get F t1 ~ alpha
|
|
| 474 | + case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
|
|
| 475 | + (Just z_tv1, _) -> try_default_tv_nom z_tv1 z_ty2
|
|
| 476 | + (_, Just z_tv2) -> try_default_tv_nom z_tv2 z_ty1
|
|
| 477 | + _ -> return False ;
|
|
| 478 | + |
|
| 479 | + ReprEq -- See Note [Defaulting representational equalities]
|
|
| 480 | + | CIrredCan (IrredCt { ir_reason }) <- ct
|
|
| 481 | + , isInsolubleReason ir_reason
|
|
| 482 | + -- Don't do this for definitely insoluble representational
|
|
| 483 | + -- equalities such as Int ~R# Bool.
|
|
| 484 | + -> return False
|
|
| 485 | + | otherwise
|
|
| 486 | + -> try_default_repr z_ty1 z_ty2
|
|
| 487 | + }
|
|
| 513 | 488 | | otherwise
|
| 514 | 489 | = return False
|
| 515 | 490 | |
| 516 | 491 | where
|
| 517 | - try_default_tv lhs_tv rhs_ty
|
|
| 492 | + -- try_default_tv_nom: used for tv ~#N ty
|
|
| 493 | + try_default_tv_nom lhs_tv rhs_ty
|
|
| 518 | 494 | | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv
|
| 519 | 495 | , tyVarKind lhs_tv `tcEqType` typeKind rhs_ty
|
| 520 | 496 | , checkTopShape info rhs_ty
|
| ... | ... | @@ -556,6 +532,33 @@ defaultEquality ct |
| 556 | 532 | ; return True
|
| 557 | 533 | }
|
| 558 | 534 | |
| 535 | + try_default_repr z_ty1 z_ty2
|
|
| 536 | + = do { traceTcS "defaultEquality ReprEq {" $ vcat
|
|
| 537 | + [ text "ct:" <+> ppr ct
|
|
| 538 | + , text "z_ty1:" <+> ppr z_ty1
|
|
| 539 | + , text "z_ty2:" <+> ppr z_ty2
|
|
| 540 | + ]
|
|
| 541 | + -- Promote this representational equality to a nominal equality.
|
|
| 542 | + --
|
|
| 543 | + -- This handles cases such as @IO alpha[tau] ~R# IO Int@
|
|
| 544 | + -- by defaulting @alpha := Int@, which is useful in practice
|
|
| 545 | + -- (see Note [Defaulting representational equalities]).
|
|
| 546 | + ; (co, new_eqs, _unifs) <-
|
|
| 547 | + wrapUnifierX (ctEvidence ct) Nominal $ \uenv ->
|
|
| 548 | + -- NB: nominal equality!
|
|
| 549 | + uType uenv z_ty1 z_ty2
|
|
| 550 | + |
|
| 551 | + -- Only accept this solution if no new equalities are produced
|
|
| 552 | + -- by the unifier.
|
|
| 553 | + --
|
|
| 554 | + -- See Note [Defaulting representational equalities].
|
|
| 555 | + ; if null new_eqs
|
|
| 556 | + then do { traceTcS "defaultEquality ReprEq } (yes)" empty
|
|
| 557 | + ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
|
|
| 558 | + evCoercion $ mkSubCo co
|
|
| 559 | + ; return True }
|
|
| 560 | + else do { traceTcS "defaultEquality ReprEq } (no)" empty
|
|
| 561 | + ; return False } }
|
|
| 559 | 562 | |
| 560 | 563 | combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
|
| 561 | 564 | combineStrategies default1 default2 ct
|
| ... | ... | @@ -2007,9 +2007,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs |
| 2007 | 2007 | swap_and_finish tv can_rhs =
|
| 2008 | 2008 | swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
|
| 2009 | 2009 | |
| 2010 | - -- We can unify; go ahead and do so.
|
|
| 2010 | + -- Phew! Finally! We can unify; go ahead and do so.
|
|
| 2011 | 2011 | unify tv rhs_redn =
|
| 2012 | - |
|
| 2013 | 2012 | do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
|
| 2014 | 2013 | -- the evidence, even if swapped=IsSwapped. Suppose the original was
|
| 2015 | 2014 | -- [W] co : Int ~ alpha
|
| ... | ... | @@ -3,7 +3,7 @@ RecordDotSyntaxFail10.hs:40:11: error: [GHC-39999] |
| 3 | 3 | • In the second argument of ‘($)’, namely ‘a {foo.bar.baz.quux}’
|
| 4 | 4 | In a stmt of a 'do' block: print $ a {foo.bar.baz.quux}
|
| 5 | 5 | In the expression:
|
| 6 | - do let a = Foo {foo = Bar {bar = ...}}
|
|
| 6 | + do let a = ...
|
|
| 7 | 7 | let quux = "Expecto patronum!"
|
| 8 | 8 | print $ a {foo.bar.baz.quux}
|
| 9 | 9 |
| ... | ... | @@ -5,6 +5,6 @@ RecordDotSyntaxFail13.hs:26:11: error: [GHC-39999] |
| 5 | 5 | • In the second argument of ‘($)’, namely ‘a {foo}’
|
| 6 | 6 | In a stmt of a 'do' block: print $ a {foo}
|
| 7 | 7 | In the expression:
|
| 8 | - do let a = Foo {foo = 12}
|
|
| 8 | + do let a = ...
|
|
| 9 | 9 | print $ a {foo}
|
| 10 | 10 |
| 1 | -exists Nothing :: Floop a mp => Existential mp |
|
| 1 | +exists Nothing :: Floop a kp => Existential kp |
| 1 | 1 | {-# LANGUAGE Haskell2010 #-}
|
| 2 | -{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
|
|
| 2 | +{-# LANGUAGE TypeFamilies, TypeFamilyDependencies, TypeOperators #-}
|
|
| 3 | 3 | module T13651 where
|
| 4 | 4 | |
| 5 | 5 | type family F r s = f | f -> r s
|
| 1 | 1 | T19415.hs:27:8: error: [GHC-18872]
|
| 2 | - • Couldn't match type ‘[Char]’ with ‘Char’
|
|
| 3 | - arising from a functional dependency between:
|
|
| 4 | - constraint ‘SetField "name" (Pet a1) (Pet b) Char’
|
|
| 5 | - arising from a use of ‘setField’
|
|
| 6 | - instance ‘SetField "name" (Pet a) (Pet b1) String’
|
|
| 7 | - at T19415.hs:(23,3)-(24,60)
|
|
| 2 | + • No instance for ‘SetField "name" (Pet a0) (Pet b0) Char’
|
|
| 3 | + arising from a use of ‘setField’
|
|
| 8 | 4 | • In the expression: setField @"name" 'c' (Pet "hi")
|
| 9 | 5 | In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi") |
| 10 | - |