[GHC] #14749: T13822 fails

[GHC]

#14749: T13822 fails
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.  But an apparently unrelated
> patch makes it fail Lint even in stage 2.  I conclude that the bug is not
> in the unrelated patch; it is somehow there all along.
>
> 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)
> }}}

New description:

 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)
 }}}

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14749#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler