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 Wibbles - - - - - 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: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -468,53 +468,29 @@ defaultEquality ct z_ty1 <- TcS.zonkTcType ty1 ; z_ty2 <- TcS.zonkTcType ty2 ; case eq_rel of - { NomEq -> - -- Now see if either LHS or RHS is a bare type variable - -- You might think the type variable will only be on the LHS - -- but with a type function we might get F t1 ~ alpha - case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of - (Just z_tv1, _) -> try_default_tv z_tv1 z_ty2 - (_, Just z_tv2) -> try_default_tv z_tv2 z_ty1 - _ -> return False ; - - ; ReprEq - -- See Note [Defaulting representational equalities] - | CIrredCan (IrredCt { ir_reason }) <- ct - , isInsolubleReason ir_reason - -- Don't do this for definitely insoluble representational - -- equalities such as Int ~R# Bool. - -> return False - | otherwise - -> - do { traceTcS "defaultEquality ReprEq {" $ vcat - [ text "ct:" <+> ppr ct - , text "z_ty1:" <+> ppr z_ty1 - , text "z_ty2:" <+> ppr z_ty2 - ] - -- Promote this representational equality to a nominal equality. - -- - -- This handles cases such as @IO alpha[tau] ~R# IO Int@ - -- by defaulting @alpha := Int@, which is useful in practice - -- (see Note [Defaulting representational equalities]). - ; (co, new_eqs, _unifs) <- - wrapUnifierX (ctEvidence ct) Nominal $ - -- NB: nominal equality! - \ uenv -> uType uenv z_ty1 z_ty2 - -- Only accept this solution if no new equalities are produced - -- by the unifier. - -- - -- See Note [Defaulting representational equalities]. - ; if null new_eqs - then do { setEvBindIfWanted (ctEvidence ct) EvCanonical $ - (evCoercion $ mkSubCo co) - ; return True } - else return False - } } } + NomEq -> -- Now see if either LHS or RHS is a bare type variable + -- You might think the type variable will only be on the LHS + -- but with a type function we might get F t1 ~ alpha + case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of + (Just z_tv1, _) -> try_default_tv_nom z_tv1 z_ty2 + (_, Just z_tv2) -> try_default_tv_nom z_tv2 z_ty1 + _ -> return False ; + + ReprEq -- See Note [Defaulting representational equalities] + | CIrredCan (IrredCt { ir_reason }) <- ct + , isInsolubleReason ir_reason + -- Don't do this for definitely insoluble representational + -- equalities such as Int ~R# Bool. + -> return False + | otherwise + -> try_default_repr z_ty1 z_ty2 + } | otherwise = return False where - try_default_tv lhs_tv rhs_ty + -- try_default_tv_nom: used for tv ~#N ty + try_default_tv_nom lhs_tv rhs_ty | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv , tyVarKind lhs_tv `tcEqType` typeKind rhs_ty , checkTopShape info rhs_ty @@ -556,6 +532,33 @@ defaultEquality ct ; return True } + try_default_repr z_ty1 z_ty2 + = do { traceTcS "defaultEquality ReprEq {" $ vcat + [ text "ct:" <+> ppr ct + , text "z_ty1:" <+> ppr z_ty1 + , text "z_ty2:" <+> ppr z_ty2 + ] + -- Promote this representational equality to a nominal equality. + -- + -- This handles cases such as @IO alpha[tau] ~R# IO Int@ + -- by defaulting @alpha := Int@, which is useful in practice + -- (see Note [Defaulting representational equalities]). + ; (co, new_eqs, _unifs) <- + wrapUnifierX (ctEvidence ct) Nominal $ \uenv -> + -- NB: nominal equality! + uType uenv z_ty1 z_ty2 + + -- Only accept this solution if no new equalities are produced + -- by the unifier. + -- + -- See Note [Defaulting representational equalities]. + ; if null new_eqs + then do { traceTcS "defaultEquality ReprEq } (yes)" empty + ; setEvBindIfWanted (ctEvidence ct) EvCanonical $ + evCoercion $ mkSubCo co + ; return True } + else do { traceTcS "defaultEquality ReprEq } (no)" empty + ; return False } } combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy combineStrategies default1 default2 ct ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2007,9 +2007,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs swap_and_finish tv can_rhs = swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs - -- We can unify; go ahead and do so. + -- Phew! Finally! We can unify; go ahead and do so. unify tv rhs_redn = - do { -- In the common case where rhs_redn is Refl, we don't need to rewrite -- the evidence, even if swapped=IsSwapped. Suppose the original was -- [W] co : Int ~ alpha ===================================== testsuite/tests/parser/should_fail/RecordDotSyntaxFail10.stderr ===================================== @@ -3,7 +3,7 @@ RecordDotSyntaxFail10.hs:40:11: error: [GHC-39999] • In the second argument of ‘($)’, namely ‘a {foo.bar.baz.quux}’ In a stmt of a 'do' block: print $ a {foo.bar.baz.quux} In the expression: - do let a = Foo {foo = Bar {bar = ...}} + do let a = ... let quux = "Expecto patronum!" print $ a {foo.bar.baz.quux} ===================================== testsuite/tests/parser/should_fail/RecordDotSyntaxFail13.stderr ===================================== @@ -5,6 +5,6 @@ RecordDotSyntaxFail13.hs:26:11: error: [GHC-39999] • In the second argument of ‘($)’, namely ‘a {foo}’ In a stmt of a 'do' block: print $ a {foo} In the expression: - do let a = Foo {foo = 12} + do let a = ... print $ a {foo} ===================================== testsuite/tests/polykinds/T6068.stdout ===================================== @@ -1 +1 @@ -exists Nothing :: Floop a mp => Existential mp +exists Nothing :: Floop a kp => Existential kp ===================================== testsuite/tests/typecheck/should_compile/T13651.hs ===================================== @@ -1,5 +1,5 @@ {-# LANGUAGE Haskell2010 #-} -{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-} +{-# LANGUAGE TypeFamilies, TypeFamilyDependencies, TypeOperators #-} module T13651 where type family F r s = f | f -> r s ===================================== testsuite/tests/typecheck/should_fail/T19415.stderr ===================================== @@ -1,10 +1,5 @@ T19415.hs:27:8: error: [GHC-18872] - • Couldn't match type ‘[Char]’ with ‘Char’ - arising from a functional dependency between: - constraint ‘SetField "name" (Pet a1) (Pet b) Char’ - arising from a use of ‘setField’ - instance ‘SetField "name" (Pet a) (Pet b1) String’ - at T19415.hs:(23,3)-(24,60) + • No instance for ‘SetField "name" (Pet a0) (Pet b0) Char’ + arising from a use of ‘setField’ • In the expression: setField @"name" 'c' (Pet "hi") In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi") - View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/44e59c0a4f2afd7013c12cefddcbabb5... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/44e59c0a4f2afd7013c12cefddcbabb5... You're receiving this email because of your account on gitlab.haskell.org.