Opened 5 months ago

Closed 3 months ago

Last modified 3 months ago

#14749 closed bug (fixed)

T13822 fails

Reported by: simonpj Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: TypeInType Cc:
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:

Description (last modified by simonpj)

Consider this cut-down T13822

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

module T13822 where

import Data.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
                                                                                              ':> '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
      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)

Change History (8)

comment:1 Changed 5 months ago by simonpj

Description: modified (diff)

comment:2 Changed 5 months ago by simonpj

Keywords: TypeInType added
Owner: set to goldfire

Richard, this is a seriously complicated coercion and I am lost. Could you look?

comment:3 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In efce943c/ghc:

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!

comment:4 Changed 5 months ago by goldfire

Confirmed that this is fixed by my fix to #12919.

comment:5 Changed 3 months ago by Richard Eisenberg <rae@…>

In e3dbb44f/ghc:

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.

comment:6 Changed 3 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14749

comment:7 Changed 3 months ago by Richard Eisenberg <rae@…>

In faec8d35/ghc:

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{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

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

Fixes #14066 #14749

Test cases: dependent/should_compile/{T14066a,T14749},

comment:8 Changed 3 months ago 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.

Note: See TracTickets for help on using tickets.