#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

#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 <simonpj@…>): In [changeset:"efce943ca20b55b18f948681e6b44fd892dbddd2/ghc" efce943c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="efce943ca20b55b18f948681e6b44fd892dbddd2" Add -ddump-ds-preopt This allows you to see the output immediately after desugaring but before any optimisation. I've wanted this for some time, but I was triggered into action by Trac #13032 comment:9. Interestingly, the change means that with -dcore-lint we will now Lint the output before the very simple optimiser; and this showed up Trac #14749. But that's not the fault of -ddump-ds-preopt! }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14749#comment:3> 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 <rae@…>): In [changeset:"e3dbb44f53b2f9403d20d84e27f187062755a089/ghc" e3dbb44f/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e3dbb44f53b2f9403d20d84e27f187062755a089" Fix #12919 by making the flattener homegeneous. This changes a key invariant of the flattener. Previously, flattening a type meant flattening its kind as well. But now, flattening is always homogeneous -- that is, the kind of the flattened type is the same as the kind of the input type. This is achieved by various wizardry in the TcFlatten.flatten_many function, as described in Note [flatten_many]. There are several knock-on effects, including some refactoring in the canonicalizer to take proper advantage of the flattener's changed behavior. In particular, the tyvar case of can_eq_nc' no longer needs to take casts into account. Another effect is that flattening a tyconapp might change it into a casted tyconapp. This might happen if the result kind of the tycon contains a variable, and that variable changes during flattening. Because the flattener is homogeneous, it tacks on a cast to keep the tyconapp kind the same. However, this is problematic when flattening CFunEqCans, which need to have an uncasted tyconapp on the LHS and must remain homogeneous. The solution is a more involved canCFunEqCan, described in Note [canCFunEqCan]. This patch fixes #13643 (as tested in typecheck/should_compile/T13643) and the panic in typecheck/should_compile/T13822 (as reported in #14024). Actually, there were two bugs in T13822: the first was just some incorrect logic in tryFill (part of the unflattener) -- also fixed in this patch -- and the other was the main bug fixed in this ticket. The changes in this patch exposed a long-standing flaw in OptCoercion, in that breaking apart an AppCo sometimes has unexpected effects on kinds. See new Note [EtaAppCo] in OptCoercion, which explains the problem and fix. Also here is a reversion of the major change in 09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion. It turns out that making the flattener homogeneous changes the invariants on the algorithm, making the change in that patch no longer necessary. This patch also fixes: #14038 (dependent/should_compile/T14038) #13910 (dependent/should_compile/T13910) #13938 (dependent/should_compile/T13938) #14441 (typecheck/should_compile/T14441) #14556 (dependent/should_compile/T14556) #14720 (dependent/should_compile/T14720) #14749 (typecheck/should_compile/T14749) Sadly, this patch negatively affects performance of type-family- heavy code. The following patch fixes these performance degradations. However, the performance fixes are somewhat invasive and so I've kept them as a separate patch, labeling this one as [skip ci] so that validation doesn't fail on the performance cases. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14749#comment:5> 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 <rae@…>): In [changeset:"faec8d358985e5d0bf363bd96f23fe76c9e281f7/ghc" faec8d35/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="faec8d358985e5d0bf363bd96f23fe76c9e281f7" Track type variable scope more carefully. The main job of this commit is to track more accurately the scope of tyvars introduced by user-written foralls. For example, it would be to have something like this: forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool In that type, a's kind must be k, but k isn't in scope. We had a terrible way of doing this before (not worth repeating or describing here, but see the old tcImplicitTKBndrs and friends), but now we have a principled approach: make an Implication when kind-checking a forall. Doing so then hooks into the existing machinery for preventing skolem-escape, performing floating, etc. This also means that we bump the TcLevel whenever going into a forall. The new behavior is done in TcHsType.scopeTyVars, but see also TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant rewriting. There are several Notes near there to guide you. Of particular interest there is that Implication constraints can now have skolems that are out of order; this situation is reported in TcErrors. A major consequence of this is a slightly tweaked process for type- checking type declarations. The new Note [Use SigTvs in kind-checking pass] in TcTyClsDecls lays it out. The error message for dependent/should_fail/TypeSkolEscape has become noticeably worse. However, this is because the code in TcErrors goes to some length to preserve pre-8.0 error messages for kind errors. It's time to rip off that plaster and get rid of much of the kind-error-specific error messages. I tried this, and doing so led to a lovely error message for TypeSkolEscape. So: I'm accepting the error message quality regression for now, but will open up a new ticket to fix it, along with a larger error-message improvement I've been pondering. This applies also to dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142. Other minor changes: - isUnliftedTypeKind didn't look for tuples and sums. It does now. - check_type used check_arg_type on both sides of an AppTy. But the left side of an AppTy isn't an arg, and this was causing a bad error message. I've changed it to use check_type on the left-hand side. - Some refactoring around when we print (TYPE blah) in error messages. The changes decrease the times when we do so, to good effect. Of course, this is still all controlled by -fprint-explicit-runtime-reps Fixes #14066 #14749 Test cases: dependent/should_compile/{T14066a,T14749}, dependent/should_fail/T14066{,c,d,e,f,g,h} }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14749#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler