[Git][ghc/ghc][wip/T23134] Fix unification with oversaturated type families

[Krzysztof Gogolewski (@monoidal)]

Krzysztof Gogolewski pushed to branch wip/T23134 at Glasgow Haskell Compiler / GHC


Commits:
3e8e00c8 by Krzysztof Gogolewski at 2023-03-20T17:25:21+01:00
Fix unification with oversaturated type families

unify_ty was incorrectly saying that F x y ~ T x are surely apart,
where F x y is an oversaturated type family and T x is a tyconapp.
As a result, the simplifier dropped a live case alternative (#23134).

- - - - -


4 changed files:

- compiler/GHC/Core/Unify.hs
- + testsuite/tests/simplCore/should_run/T23134.hs
- + testsuite/tests/simplCore/should_run/T23134.stdout
- testsuite/tests/simplCore/should_run/all.T


Changes:

=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1061,6 +1061,20 @@ unify_ty env ty1 ty2 _kco
   , um_unif env               -- behaves like a type variable; might unify
   = maybeApart MARTypeFamily
 
+  -- An oversaturated type family can match a TyConApp,
+  -- this is handled the same way as in the AppTy case below (#23134)
+  | Just (tc1, _) <- mb_tc_app1
+  , isTypeFamilyTyCon tc1
+  , Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+  , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+  = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
+
+  | Just (tc2, _) <- mb_tc_app2
+  , isTypeFamilyTyCon tc2
+  , Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+  , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+  = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
+
   -- TYPE and CONSTRAINT are not Apart
   -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
   -- NB: at this point we know that the two TyCons do not match


=====================================
testsuite/tests/simplCore/should_run/T23134.hs
=====================================
@@ -0,0 +1,37 @@
+{-# LANGUAGE GHC2021, DataKinds, TypeFamilies #-}
+module Main where
+
+import Data.Maybe
+import Data.Kind
+
+main :: IO ()
+main = putStrLn str
+
+str :: String
+str = case runInstrImpl @(TOption TUnit) mm MAP of
+         C VOption -> "good"
+         C Unused -> "bad"
+
+runInstrImpl :: forall inp out. Value (MapOpRes inp TUnit) -> Instr inp out -> Rec out
+runInstrImpl m MAP = C m
+
+type MapOpRes :: T -> T -> T
+type family MapOpRes c :: T -> T
+type instance MapOpRes ('TOption x) = 'TOption
+
+mm :: Value (TOption TUnit)
+mm = VOption
+{-# NOINLINE mm #-}
+
+type Value :: T -> Type
+data Value t where
+  VOption :: Value ('TOption t)
+  Unused :: Value t
+
+data T = TOption T | TUnit
+
+data Instr (inp :: T) (out :: T) where
+  MAP :: Instr c (TOption (MapOpRes c TUnit))
+
+data Rec :: T -> Type where
+  C :: Value r -> Rec (TOption r)


=====================================
testsuite/tests/simplCore/should_run/T23134.stdout
=====================================
@@ -0,0 +1 @@
+good


=====================================
testsuite/tests/simplCore/should_run/all.T
=====================================
@@ -109,4 +109,5 @@ test('T21575b', [], multimod_compile_and_run, ['T21575b', '-O'])
 test('T20836', normal, compile_and_run, ['-O0']) # Should not time out; See #20836
 test('T22448', normal, compile_and_run, ['-O1'])
 test('T22998', normal, compile_and_run, ['-O0 -fspecialise -dcore-lint'])
+test('T23134', normal, compile_and_run, ['-O0 -fcatch-nonexhaustive-cases'])
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3e8e00c85d8684cab84ffe8628f54105c0b2651c

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230320/e3bc6c40/attachment-0001.html>