T13822 fails

Consider this cut-down T13822

{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}

module T13822 where

import Data.Kind

data KIND = STAR | KIND :> KIND

data Ty :: KIND -> Type where
  TMaybe :: Ty (STAR :> STAR)
  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)

type family IK (k :: KIND) = (res :: Type) where
  IK STAR   = Type
  IK (a:>b) = IK a -> IK b

type family I (t :: Ty k) = (res :: IK k)  where
  I TMaybe     = Maybe
  I (TApp f a) = (I f) (I a)

data TyRep (k :: KIND) (t :: Ty k) where
  TyMaybe :: TyRep (STAR:>STAR) TMaybe
  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)

zero :: TyRep STAR a -> I a
zero x = case x of
            TyApp TyMaybe _ -> Nothing

With a stage-1 compiler with DEBUG enabled, this program yields a Lint error in all recent versions of GHC. (NB: Lint, not an assertion failure.)

With stage-2 it succeeds, and passes Lint. Reason: without DEBUG the output of the typechecker is not Linted until after a run of the CoreOpt; and that simplifies the coercions; which somehow eliminates the Lint error.

I added-ddump-ds-preopt to made the pre-core-opt dump optional -- it is sometimes useful in a non-DEBUG compiler. But that makes Lint run on the pre-core-opt code, and that shows up the bug always. But an apparently unrelated patch makes it fail Lint even in stage 2. So it's kind of harmless; but a clear bug that we should fix.

I'll mark T13822 as expect-broken; you can re-enable it when this ticket is fixed.

The Lint error is pretty obscure

*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    [in body of letrec with binders co_a10u :: (f_a10g :: Ty
                                                            (a_a10f ':> 'STAR))
                                               ~# (('TMaybe |> (Ty
                                                                  (Sym co_a10r
                                                                   ':> <'STAR>_N)_N)_N) :: Ty
                                                                                             (a_a10f
                                                                                              ':> 'STAR))]
    Kind application error in
      coercion ‘(Maybe
                   (Sym (Coh <I (x_a10h |> Sym (Ty (Sym co_a10r))_N)>_N
                             (D:R:IK[0]) ; Coh <(I (x_a10h |> Sym (Ty
                                                                     (Sym co_a10r))_N) |> D:R:IK[0])>_N
                                               (Sym (D:R:IK[0]))) ; Coh <I (x_a10h |> Sym (Ty
                                                                                             (Sym co_a10r))_N)>_N
                                                                        (D:R:IK[0])))_N’
      Function kind = * -> *
      Arg kinds = [(I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR)]
    Fun: *
         (I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR)