[Git][ghc/ghc][master] Fix unifier bug: failing to decompose over-saturated type family

[Marge Bot (@marge-bot)]

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


Commits:
317f45c1 by Simon Peyton Jones at 2022-12-22T23:41:07-05:00
Fix unifier bug: failing to decompose over-saturated type family

This simple patch fixes #22647

- - - - -


3 changed files:

- compiler/GHC/Core/Unify.hs
- + testsuite/tests/typecheck/should_compile/T22647.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1054,20 +1054,11 @@ unify_ty env ty1 ty2 _kco
             ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
               don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
 
-  | Just (tc1, _) <- mb_tc_app1
-  , not (isGenerativeTyCon tc1 Nominal)
-    -- E.g.   unify_ty (F ty1) b  =  MaybeApart
-    --        because the (F ty1) behaves like a variable
-    --        NB: if unifying, we have already dealt
-    --            with the 'ty2 = variable' case
-  = maybeApart MARTypeFamily
+  | isTyFamApp mb_tc_app1     -- A (not-over-saturated) type-family application
+  = maybeApart MARTypeFamily  -- behaves like a type variable; might match
 
-  | Just (tc2, _) <- mb_tc_app2
-  , not (isGenerativeTyCon tc2 Nominal)
-  , um_unif env
-    -- E.g.   unify_ty [a] (F ty2) =  MaybeApart, when unifying (only)
-    --        because the (F ty2) behaves like a variable
-    --        NB: we have already dealt with the 'ty1 = variable' case
+  | isTyFamApp mb_tc_app2     -- A (not-over-saturated) type-family application
+  , um_unif env               -- behaves like a type variable; might unify
   = maybeApart MARTypeFamily
 
   -- TYPE and CONSTRAINT are not Apart
@@ -1169,6 +1160,17 @@ unify_tys env orig_xs orig_ys
       -- Possibly different saturations of a polykinded tycon
       -- See Note [Polykinded tycon applications]
 
+isTyFamApp :: Maybe (TyCon, [Type]) -> Bool
+-- True if we have a saturated or under-saturated type family application
+-- If it is /over/ saturated then we return False.  E.g.
+--     unify_ty (F a b) (c d)    where F has arity 1
+-- we definitely want to decompose that type application! (#22647)
+isTyFamApp (Just (tc, tys))
+  =  not (isGenerativeTyCon tc Nominal)       -- Type family-ish
+  && not (tys `lengthExceeds` tyConArity tc)  -- Not over-saturated
+isTyFamApp Nothing
+  = False
+
 ---------------------------------
 uVar :: UMEnv
      -> InTyVar         -- Variable to be unified


=====================================
testsuite/tests/typecheck/should_compile/T22647.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeApplications, KindSignatures, DataKinds, TypeFamilies, FlexibleInstances #-}
+
+module T22647 where
+
+import Data.Kind
+
+data D = D
+type family F :: D -> Type
+
+class C f where
+  meth :: f
+
+instance C (f (p :: D)) where   -- f :: D -> Type
+  meth = error "urk1"
+
+instance C (g (q :: Type)) where -- g :: Type -> Type
+  meth = error "urk2"
+
+x = meth :: F 'D
+
+y = meth :: [Type]


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -853,3 +853,4 @@ test('T21550', normal, compile, [''])
 test('T22310', normal, compile, [''])
 test('T22331', normal, compile, [''])
 test('T22516', normal, compile, [''])
+test('T22647', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/317f45c154f6fe25d50ef2f3febcc5883ff1b1ca

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/317f45c154f6fe25d50ef2f3febcc5883ff1b1ca
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/20221222/67d89b3c/attachment-0001.html>