Fix #16188wip/T16188

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

12 files changed, 251 insertions, 41 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index a1451a83bc..d643925127 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1576,11 +1576,15 @@ canDecomposableTyConAppOK :: CtEvidence -> EqRel
                           -> TcS ()
 -- Precondition: tys1 and tys2 are the same length, hence "OK"
 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-  = case ev of
+  = ASSERT( tys1 `equalLength` tys2 )
+    case ev of
      CtDerived {}
         -> unifyDeriveds loc tc_roles tys1 tys2
 
      CtWanted { ctev_dest = dest }
+                   -- new_locs and tc_roles are both infinite, so
+                   -- we are guaranteed that cos has the same length
+                   -- as tys1 and tys2
         -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
               ; setWantedEq dest (mkTyConAppCo role tc cos) }
 
@@ -1596,21 +1600,29 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
   where
     loc        = ctEvLoc ev
     role       = eqRelRole eq_rel
-    tc_roles   = tyConRolesX role tc
-
-      -- the following makes a better distinction between "kind" and "type"
-      -- in error messages
-    bndrs      = tyConBinders tc
-    is_kinds   = map isNamedTyConBinder bndrs
-    is_viss    = map isVisibleTyConBinder bndrs
 
-    kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
-    vis_xforms  = map (\is_vis  -> if is_vis  then id
-                                   else flip updateCtLocOrigin toInvisibleOrigin)
-                      is_viss
+      -- infinite, as tyConRolesX returns an infinite tail of Nominal
+    tc_roles   = tyConRolesX role tc
 
-    -- zipWith3 (.) composes its first two arguments and applies it to the third
-    new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
+      -- Add nuances to the location during decomposition:
+      --  * if the argument is a kind argument, remember this, so that error
+      --    messages say "kind", not "type". This is determined based on whether
+      --    the corresponding tyConBinder is named (that is, dependent)
+      --  * if the argument is invisible, note this as well, again by
+      --    looking at the corresponding binder
+      -- For oversaturated tycons, we need the (repeat loc) tail, which doesn't
+      -- do either of these changes. (Forgetting to do so led to #16188)
+      --
+      -- NB: infinite in length
+    new_locs = [ new_loc
+               | bndr <- tyConBinders tc
+               , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
+                              | otherwise               = loc
+                     new_loc  | isVisibleTyConBinder bndr
+                              = updateCtLocOrigin new_loc0 toInvisibleOrigin
+                              | otherwise
+                              = new_loc0 ]
+               ++ repeat loc
 
 -- | Call when canonicalizing an equality fails, but if the equality is
 -- representational, there is some hope for the future.
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 701c674aaf..7bb85740ac 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1317,10 +1317,13 @@ applyRoles tc cos
 -- the Role parameter is the Role of the TyConAppCo
 -- defined here because this is intimately concerned with the implementation
 -- of TyConAppCo
+-- Always returns an infinite list (with a infinite tail of Nominal)
 tyConRolesX :: Role -> TyCon -> [Role]
 tyConRolesX Representational tc = tyConRolesRepresentational tc
 tyConRolesX role             _  = repeat role
 
+-- Returns the roles of the parameters of a tycon, with an infinite tail
+-- of Nominal
 tyConRolesRepresentational :: TyCon -> [Role]
 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
 
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, [''])