Fix #16188

There was an awful lot of zipping going on in
canDecomposableTyConAppOK, and one of the lists being zipped
was too short, causing the result to be too short. Easily
fixed.

Also fixes #16204 and #16225

test case: typecheck/should_compile/T16188
           typecheck/should_compile/T16204[ab]
           typecheck/should_fail/T16204c
           typecheck/should_compile/T16225

10 files changed, 222 insertions, 27 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 93d7746066..6b1a6bd075 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,16 +1,4 @@
 
-T2544.hs:19:12: error:
-    • Couldn't match type ‘IxMap r’ with ‘IxMap i1’
-      Expected type: IxMap (l :|: r) [Int]
-        Actual type: BiApp (IxMap l) (IxMap i1) [Int]
-      NB: ‘IxMap’ is a non-injective type family
-      The type variable ‘i1’ is ambiguous
-    • In the expression: BiApp empty empty
-      In an equation for ‘empty’: empty = BiApp empty empty
-      In the instance declaration for ‘Ix (l :|: r)’
-    • Relevant bindings include
-        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
-
 T2544.hs:19:18: error:
     • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
       Expected type: IxMap l [Int]
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index f85cf66d79..41790105cb 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -24,18 +24,3 @@ T14172.hs:7:19: error:
     • 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)
diff --git a/testsuite/tests/typecheck/should_compile/T16188.hs b/testsuite/tests/typecheck/should_compile/T16188.hs
new file mode 100644
index 0000000000..31144198a3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16188.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T16188 where
+
+import Data.Kind (Type)
+import Data.Type.Bool (type (&&))
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+data family Sing :: forall k. k -> Type
+
+data instance Sing :: Bool -> Type where
+  SFalse :: Sing False
+  STrue  :: Sing True
+
+(%&&) :: forall (x :: Bool) (y :: Bool).
+         Sing x -> Sing y -> Sing (x && y)
+SFalse %&& _ = SFalse
+STrue  %&& a = a
+
+data RegExp :: Type -> Type where
+  App :: RegExp t -> RegExp t -> RegExp t
+
+data instance Sing :: forall t. RegExp t -> Type where
+  SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
+
+data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
+type instance Apply ReNotEmptySym0 r = ReNotEmpty r
+
+type family ReNotEmpty (r :: RegExp t) :: Bool where
+  ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
+
+sReNotEmpty :: forall t (r :: RegExp t).
+               Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
+sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
+
+blah :: forall (t :: Type) (re :: RegExp t).
+        Sing re -> ()
+blah (SApp sre1 sre2)
+  = case (sReNotEmpty sre1, sReNotEmpty sre2) of
+      (STrue, STrue) -> ()
diff --git a/testsuite/tests/typecheck/should_compile/T16204a.hs b/testsuite/tests/typecheck/should_compile/T16204a.hs
new file mode 100644
index 0000000000..63cae41d8c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16204a.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204 where
+
+import Data.Kind
+
+-----
+-- singletons machinery
+-----
+
+data family Sing :: forall k. k -> Type
+data SomeSing :: Type -> Type where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+-----
+-- (Simplified) GHC.Generics
+-----
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to   :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  -- type PFrom ...
+  type PTo (x :: Rep a) :: a
+
+class SGeneric k where
+  -- sFrom :: ...
+  sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+-----
+
+class SingKind k where
+  type Demote k :: Type
+  -- fromSing :: ...
+  toSing :: Demote k -> SomeSing k
+
+genericToSing :: forall k.
+                 ( SingKind k, SGeneric k, SingKind (Rep k)
+                 , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
+              => Demote k -> SomeSing k
+genericToSing d = withSomeSing @(Rep k) (from d) $ SomeSing . sTo
+
+withSomeSing :: forall k r
+              . SingKind k
+             => Demote k
+             -> (forall (a :: k). Sing a -> r)
+             -> r
+withSomeSing x f =
+  case toSing x of
+    SomeSing x' -> f x'
diff --git a/testsuite/tests/typecheck/should_compile/T16204b.hs b/testsuite/tests/typecheck/should_compile/T16204b.hs
new file mode 100644
index 0000000000..12f7391f49
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16204b.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204b where
+
+import Data.Kind
+
+-----
+-- singletons machinery
+-----
+
+data family Sing :: forall k. k -> Type
+data SomeSing :: Type -> Type where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+-----
+-- (Simplified) GHC.Generics
+-----
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to   :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  -- type PFrom ...
+  type PTo (x :: Rep a) :: a
+
+class SGeneric k where
+  -- sFrom :: ...
+  sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+-----
+
+class SingKind k where
+  type Demote k :: Type
+  -- fromSing :: ...
+  toSing :: Demote k -> SomeSing k
+
+genericToSing :: forall k.
+                 ( SingKind k, SGeneric k, SingKind (Rep k)
+                 , Generic (Demote k), Rep (Demote k) ~ Demote (Rep k) )
+              => Demote k -> SomeSing k
+genericToSing d = withSomeSing (from d) $ SomeSing . sTo
+
+withSomeSing :: forall k r
+              . SingKind k
+             => Demote k
+             -> (forall (a :: k). Sing a -> r)
+             -> r
+withSomeSing x f =
+  case toSing x of
+    SomeSing x' -> f x'
diff --git a/testsuite/tests/typecheck/should_compile/T16225.hs b/testsuite/tests/typecheck/should_compile/T16225.hs
new file mode 100644
index 0000000000..85c5441327
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16225.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T16225 where
+
+import Data.Kind
+
+data family Sing :: k -> Type
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+
+data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
+type instance Apply (TyCon1 f) x = f x
+
+data SomeApply :: (k ~> Type) -> Type where
+  SomeApply :: Apply f a -> SomeApply f
+
+f :: SomeApply (TyCon1 Sing :: k ~> Type)
+  -> SomeApply (TyCon1 Sing :: k ~> Type)
+f (SomeApply s)
+ = SomeApply s
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3ee0a9f6d4..dae5b6feea 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -665,3 +665,7 @@ test('T16033', normal, compile, [''])
 test('T16141', normal, compile, ['-O'])
 test('T15549a', normal, compile, [''])
 test('T15549b', normal, compile, [''])
+test('T16188', normal, compile, [''])
+test('T16204a', normal, compile, [''])
+test('T16204b', normal, compile, [''])
+test('T16225', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.hs b/testsuite/tests/typecheck/should_fail/T16204c.hs
new file mode 100644
index 0000000000..97318a5729
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16204c.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16204c where
+
+import Data.Kind
+
+data family Sing :: forall k. k -> Type
+type family Rep  :: Type
+
+sTo :: forall (a :: Rep). Sing a
+sTo = sTo
+
+x :: forall (a :: Type). Sing a
+x = id sTo
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.stderr b/testsuite/tests/typecheck/should_fail/T16204c.stderr
new file mode 100644
index 0000000000..48d63785ad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16204c.stderr
@@ -0,0 +1,12 @@
+
+T16204c.hs:16:8: error:
+    • Couldn't match kind ‘Rep’ with ‘*’
+      When matching types
+        a0 :: Rep
+        a :: *
+      Expected type: Sing a
+        Actual type: Sing a0
+    • In the first argument of ‘id’, namely ‘sTo’
+      In the expression: id sTo
+      In an equation for ‘x’: x = id sTo
+    • Relevant bindings include x :: Sing a (bound at T16204c.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 52f02cfcf5..3f7e820d05 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -510,3 +510,4 @@ test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail,
 test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059e', '-v0'])
 test('T16255', normal, compile_fail, [''])
+test('T16204c', normal, compile_fail, [''])