[GHC] #14749: T13822 fails

#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

#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 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) }}}
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 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#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14749: T13822 fails -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire * keywords: => TypeInType Comment: Richard, this is a seriously complicated coercion and I am lost. Could you look? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14749#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

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

#14749: T13822 fails -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Confirmed that this is fixed by my fix to #12919. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14749#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

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

#14749: T13822 fails -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T14749 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => typecheck/should_compile/T14749 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14749#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14749: T13822 fails
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: goldfire
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.2
Resolution: fixed | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| typecheck/should_compile/T14749
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#14749: T13822 fails -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T14749 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Hmm. In retrospect, I'm not sure which of these commits (which I've worked on together) actually nailed this one. But it's nailed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14749#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC