Add regression test for #14172

Commit 433b80de fixed #14172. Let's
add a regression test to ensure that it stays fixed.

testsuite/tests/polykinds/T14172.hs

+module T14172 where
+
+import Data.Functor.Compose
+import T14172a
+
+traverseCompose :: (a -> f b) -> g a -> f (h _)
+traverseCompose = _Wrapping Compose . traverse

testsuite/tests/polykinds/T14172.stderr

+
+T14172.hs:6:46: error:
+    • Found type wildcard ‘_’ standing for ‘a'’
+      Where: ‘a'’ is a rigid type variable bound by
+               the inferred type of
+                 traverseCompose :: (a -> f b) -> g a -> f (h a')
+               at T14172.hs:7:1-46
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature:
+        traverseCompose :: (a -> f b) -> g a -> f (h _)
+
+T14172.hs:7:19: error:
+    • Occurs check: cannot construct the infinite type: a ~ g'1 a
+      Expected type: (f'0 a -> f (f'0 b))
+                     -> Compose f'0 g'1 a -> f (h a')
+        Actual type: (Unwrapped (Compose f'0 g'1 a)
+                      -> f (Unwrapped (h a')))
+                     -> Compose f'0 g'1 a -> f (h a')
+    • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
+      In the expression: _Wrapping Compose . traverse
+      In an equation for ‘traverseCompose’:
+          traverseCompose = _Wrapping Compose . traverse
+    • Relevant bindings include
+        traverseCompose :: (a -> f b) -> g a -> f (h a')
+          (bound at T14172.hs:7:1)
+
+T14172.hs:7:19: error:
+    • Couldn't match type ‘g’ with ‘Compose f'0 g'1’
+      ‘g’ is a rigid type variable bound by
+        the inferred type of
+          traverseCompose :: (a -> f b) -> g a -> f (h a')
+        at T14172.hs:7:1-46
+      Expected type: (a -> f b) -> g a -> f (h a')
+        Actual type: (a -> f b) -> Compose f'0 g'1 a -> f (h a')
+    • In the expression: _Wrapping Compose . traverse
+      In an equation for ‘traverseCompose’:
+          traverseCompose = _Wrapping Compose . traverse
+    • Relevant bindings include
+        traverseCompose :: (a -> f b) -> g a -> f (h a')
+          (bound at T14172.hs:7:1)

testsuite/tests/polykinds/T14172a.hs

+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14172a where
+
+import Data.Coerce
+import Data.Functor.Compose
+import Data.Functor.Identity
+
+class Profunctor p where
+  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+  (#.) :: Coercible c b => (b -> c) -> p a b -> p a c
+
+instance Profunctor (->) where
+  dimap ab cd bc = cd . bc . ab
+  {-# INLINE dimap #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
+
+type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
+type Iso' s a = Iso s s a a
+
+iso :: (s -> a) -> (b -> t) -> Iso s t a b
+iso sa bt = dimap sa (fmap bt)
+{-# INLINE iso #-}
+
+type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)
+
+data Exchange a b s t = Exchange (s -> a) (b -> t)
+
+instance Profunctor (Exchange a b) where
+  dimap f g (Exchange sa bt) = Exchange (sa . f) (g . bt)
+  {-# INLINE dimap #-}
+  (#.) _ = coerce
+  {-# INLINE ( #. ) #-}
+
+withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+withIso ai k = case ai (Exchange id Identity) of
+  Exchange sa bt -> k sa (runIdentity #. bt)
+{-# INLINE withIso #-}
+
+class Wrapped s where
+  type Unwrapped s :: *
+  _Wrapped' :: Iso' s (Unwrapped s)
+
+class Wrapped s => Rewrapped (s :: *) (t :: *)
+
+class    (Rewrapped s t, Rewrapped t s) => Rewrapping s t
+instance (Rewrapped s t, Rewrapped t s) => Rewrapping s t
+
+instance (t ~ Compose f' g' a') => Rewrapped (Compose f g a) t
+instance Wrapped (Compose f g a) where
+  type Unwrapped (Compose f g a) = f (g a)
+  _Wrapped' = iso getCompose Compose
+
+_Wrapping :: Rewrapping s t => (Unwrapped s -> s) -> Iso s t (Unwrapped s) (Unwrapped t)
+_Wrapping _ = _Wrapped
+{-# INLINE _Wrapping #-}
+
+_Wrapped :: Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
+_Wrapped = withIso _Wrapped' $ \ sa _ -> withIso _Wrapped' $ \ _ bt -> iso sa bt
+{-# INLINE _Wrapped #-}

testsuite/tests/polykinds/all.T

@@ -174,6 +174,7 @@ test('T13391', normal, compile_fail, [''])
 test('T13391a', normal, compile, [''])
 test('T14270', normal, compile, [''])
 test('T14450', normal, compile_fail, [''])
+test('T14172', normal, multimod_compile_fail, ['T14172.hs','-v0'])
 test('T14174', normal, compile_fail, [''])
 test('T14174a', normal, compile, [''])
 test('T14520', normal, compile_fail, [''])