[Git][ghc/ghc][master] Use mkTrAppChecked in ds_ev_typeable

8 May 2025


      Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
9c6d2b1b by sheaf at 2025-05-08T06:22:11-04:00
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

- - - - -


5 changed files:

- compiler/GHC/Builtin/Names.hs
- compiler/GHC/HsToCore/Binds.hs
- + testsuite/tests/typecheck/should_run/T25998.hs
- + testsuite/tests/typecheck/should_run/T25998.stdout
- testsuite/tests/typecheck/should_run/all.T


Changes:

=====================================
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


=====================================
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
        }
 


=====================================
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 @(->))


=====================================
testsuite/tests/typecheck/should_run/T25998.stdout
=====================================
@@ -0,0 +1,2 @@
+Equal!
+


=====================================
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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9c6d2b1bf54310b6d9755aa2ba67fbe3...

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9c6d2b1bf54310b6d9755aa2ba67fbe3...
You're receiving this email because of your account on gitlab.haskell.org.

    

[Git][ghc/ghc][master] Use mkTrAppChecked in ds_ev_typeable

Marge Bot (＠marge-bot)