[GHC] #14749: T13822 fails

1 Feb 2018

      #14749: T13822 fails
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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  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  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
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler