summaryrefslogtreecommitdiff
path: root/compiler/GHC
diff options
context:
space:
mode:
authorAdam Gundry <adam@well-typed.com>2021-03-09 10:28:37 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-04-14 19:42:18 -0400
commit5f1722994dc29a86f5495ebafb15475a46b0532c (patch)
tree5f1dba84f8b34a392981aa3dedb8fceeaee75c7d /compiler/GHC
parent79e5c8674d6bc46312efb31101889001951769d7 (diff)
downloadhaskell-5f1722994dc29a86f5495ebafb15475a46b0532c.tar.gz
Add isInjectiveTyCon check to opt_univ (fixes #19509)
Diffstat (limited to 'compiler/GHC')
-rw-r--r--compiler/GHC/Core/Coercion/Opt.hs18
1 files changed, 18 insertions, 0 deletions
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 4783ac6fe1..66ba8ee8ab 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -502,6 +502,23 @@ of arguments in a `CoTyConApp` can differ. Consider
Any (*->*) Maybe Int :: *
Hence the need to compare argument lengths; see #13658
+
+Note [opt_univ needs injectivity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If opt_univ sees a coercion between `T a1 a2` and `T b1 b2` it will optimize it
+by producing a TyConAppCo for T, and pushing the UnivCo into the arguments. But
+this works only if T is injective. Otherwise we can have something like
+
+ type family F x where
+ F Int = Int
+ F Bool = Int
+
+where `UnivCo :: F Int ~ F Bool` is reasonable (it is effectively just an
+alternative representation for a couple of uses of AxiomInstCos) but we do not
+want to produce `F (UnivCo :: Int ~ Bool)` where the inner coercion is clearly
+inconsistent. Hence the opt_univ case for TyConApps checks isInjectiveTyCon.
+See #19509.
+
-}
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
@@ -518,6 +535,7 @@ opt_univ env sym prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
, tc1 == tc2
+ , isInjectiveTyCon tc1 role -- see Note [opt_univ needs injectivity]
, equalLength tys1 tys2 -- see Note [Differing kinds]
-- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
-- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps