From 9c6d2b1bf54310b6d9755aa2ba67fbe38feeac51 Mon Sep 17 00:00:00 2001
From: sheaf <sam.derbyshire@gmail.com>
Date: Tue, 29 Apr 2025 17:42:44 +0200
Subject: [PATCH] Use mkTrAppChecked in ds_ev_typeable
This change avoids violating the invariant of mkTrApp according to which
the argument should not be a fully saturated function type.
This ensures we don't return false negatives for type equality
involving function types.
Fixes #25998
---
compiler/GHC/Builtin/Names.hs | 10 ++++-----
compiler/GHC/HsToCore/Binds.hs | 10 ++++-----
.../tests/typecheck/should_run/T25998.hs | 21 +++++++++++++++++++
.../tests/typecheck/should_run/T25998.stdout | 2 ++
testsuite/tests/typecheck/should_run/all.T | 1 +
5 files changed, 34 insertions(+), 10 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_run/T25998.hs
create mode 100644 testsuite/tests/typecheck/should_run/T25998.stdout
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 92640ad7138..0dae6bfd8fe 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -245,7 +245,7 @@ basicKnownKeyNames
typeRepIdName,
mkTrTypeName,
mkTrConName,
- mkTrAppName,
+ mkTrAppCheckedName,
mkTrFunName,
typeSymbolTypeRepName, typeNatTypeRepName, typeCharTypeRepName,
trGhcPrimModuleName,
@@ -1356,7 +1356,7 @@ typeableClassName
, someTypeRepDataConName
, mkTrTypeName
, mkTrConName
- , mkTrAppName
+ , mkTrAppCheckedName
, mkTrFunName
, typeRepIdName
, typeNatTypeRepName
@@ -1371,7 +1371,7 @@ someTypeRepDataConName = dcQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "SomeTypeR
typeRepIdName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "typeRep#") typeRepIdKey
mkTrTypeName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "mkTrType") mkTrTypeKey
mkTrConName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "mkTrCon") mkTrConKey
-mkTrAppName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "mkTrApp") mkTrAppKey
+mkTrAppCheckedName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "mkTrAppChecked") mkTrAppCheckedKey
mkTrFunName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "mkTrFun") mkTrFunKey
typeNatTypeRepName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "typeNatTypeRep") typeNatTypeRepKey
typeSymbolTypeRepName = varQual gHC_INTERNAL_TYPEABLE_INTERNAL (fsLit "typeSymbolTypeRep") typeSymbolTypeRepKey
@@ -2499,7 +2499,7 @@ proxyHashKey = mkPreludeMiscIdUnique 502
mkTyConKey
, mkTrTypeKey
, mkTrConKey
- , mkTrAppKey
+ , mkTrAppCheckedKey
, mkTrFunKey
, typeNatTypeRepKey
, typeSymbolTypeRepKey
@@ -2509,7 +2509,7 @@ mkTyConKey
mkTyConKey = mkPreludeMiscIdUnique 503
mkTrTypeKey = mkPreludeMiscIdUnique 504
mkTrConKey = mkPreludeMiscIdUnique 505
-mkTrAppKey = mkPreludeMiscIdUnique 506
+mkTrAppCheckedKey = mkPreludeMiscIdUnique 506
typeNatTypeRepKey = mkPreludeMiscIdUnique 507
typeSymbolTypeRepKey = mkPreludeMiscIdUnique 508
typeCharTypeRepKey = mkPreludeMiscIdUnique 509
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 2e025ddf96e..9534cc52681 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -1850,14 +1850,14 @@ ds_ev_typeable ty (EvTypeableTyApp ev1 ev2)
| Just (t1,t2) <- splitAppTy_maybe ty
= do { e1 <- getRep ev1 t1
; e2 <- getRep ev2 t2
- ; mkTrApp <- dsLookupGlobalId mkTrAppName
- -- mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
- -- TypeRep a -> TypeRep b -> TypeRep (a b)
+ ; mkTrAppChecked <- dsLookupGlobalId mkTrAppCheckedName
+ -- mkTrAppChecked :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+ -- TypeRep a -> TypeRep b -> TypeRep (a b)
; let (_, k1, k2) = splitFunTy (typeKind t1) -- drop the multiplicity,
-- since it's a kind
- ; let expr = mkApps (mkTyApps (Var mkTrApp) [ k1, k2, t1, t2 ])
+ ; let expr = mkApps (mkTyApps (Var mkTrAppChecked) [ k1, k2, t1, t2 ])
[ e1, e2 ]
- -- ; pprRuntimeTrace "Trace mkTrApp" (ppr expr) expr
+ -- ; pprRuntimeTrace "Trace mkTrAppChecked" (ppr expr) expr
; return expr
}
diff --git a/testsuite/tests/typecheck/should_run/T25998.hs b/testsuite/tests/typecheck/should_run/T25998.hs
new file mode 100644
index 00000000000..65df2c70446
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T25998.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main where
+
+import Data.Kind
+import Type.Reflection
+
+test :: forall (a :: Type) (b :: Type). TypeRep a -> TypeRep b -> String
+test a b = case eqTypeRep a b of
+ Just _ -> "Equal!\n"
+ Nothing -> "Not equal:\n" <> show a <> "\n" <> show b <> "\n"
+
+combine :: forall (t :: Type -> Type -> Type). Typeable t => TypeRep (t Bool Int)
+combine = typeRep
+
+main :: IO ()
+main = do
+ putStrLn $ test (typeRep @(Bool -> Int)) (combine @(->))
diff --git a/testsuite/tests/typecheck/should_run/T25998.stdout b/testsuite/tests/typecheck/should_run/T25998.stdout
new file mode 100644
index 00000000000..faab95d345d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T25998.stdout
@@ -0,0 +1,2 @@
+Equal!
+
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 1dd52653394..485da805dd3 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -173,6 +173,7 @@ test('T23761', normal, compile_and_run, [''])
test('T25529', normal, compile_and_run, [''])
test('T23761b', normal, compile_and_run, [''])
test('T17594e', normal, compile_and_run, [''])
+test('T25998', normal, compile_and_run, [''])
# Tests for expanding do before typechecking (Impredicative + RebindableSyntax)
test('T18324', normal, compile_and_run, [''])
--
GitLab