Opened 17 months ago

Closed 6 months ago

#13643 closed bug (fixed)

Core lint error with TypeInType and TypeFamilyDependencies

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: InjectiveFamilies, TypeInType Cc: int-index
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T13643
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

In the code

{-# Language TypeFamilyDependencies #-}
{-# Language RankNTypes             #-}
{-# Language KindSignatures         #-}
{-# Language DataKinds              #-}
{-# Language TypeInType             #-}
{-# Language GADTs                  #-}

import Data.Kind (Type)

data Code = I

type family
  Interp (a :: Code) = (res :: Type) | res -> a where
  Interp I = Bool

data T :: forall a. Interp a -> Type where
  MkNat :: T False

instance Show (T a) where show _ = "MkNat"

main = do
  print MkNat

but add {-# Options_GHC -dcore-lint #-} and we get the attached log from running runghc /tmp/tPb2.hs > /tmp/tPb2.log.

Attachments (1)

tPb2.log (3.7 KB) - added by Iceland_jack 17 months ago.

Download all attachments as: .zip

Change History (8)

Changed 17 months ago by Iceland_jack

Attachment: tPb2.log added

comment:1 Changed 17 months ago by Iceland_jack

comment:2 Changed 17 months ago by goldfire

I believe this is the same as #12919, although the symptoms are markedly different.

The problem is that (because flattened types have flattened kinds), flattening T I (False |> co) (where co :: Bool ~ Interp I) yields the ill-kinded T I False. Instead, we should change the kind invariant on flattening to say that flattening does not change a type's kind. Then this problem (and #12919) are fixed. I hope.

comment:3 Changed 17 months ago by simonpj

With HEAD I get

<no location info>: warning:
    In the expression: $fShowT @ 'I @ 'False
    Kinds don't match in type application:
    Type variable: a2_a18K :: Interp 'I
    Arg type: 'False :: Bool
    Linted Arg kind: Bool
<no location info>: warning:
    In the type ‘Show (T 'I 'False)’
    Kind application error in type ‘T 'I 'False’
      Function kind = forall (a :: Code). Interp a -> *
      Arg kinds = [('I, Code), ('False, Bool)]
<no location info>: warning:
    [RHS of $dShow_a18r :: Show (T 'I ('False |> Sym (D:R:Interp[0])))]
    Kind application error in
      coercion ‘(T <'I>_N
                   (Sym (Coh (Sym (Coh <'False>_N
                                       (Trans (Sym (D:R:Interp[0])) (D:R:Interp[0]))))
                             (Sym (D:R:Interp[0])))))_N’
      Function kind = forall (a :: Code). Interp a -> *
      Arg kinds = [('I, Code), ('False, Bool)]

Look at at the type in the second error:

    In the type ‘Show (T 'I 'False)’

It's ill-kinded! I discussed with Richard and this is just another example of #12919. Consider what happens if we flatten

  T 'I ('False |> g)

we'll get the flattened type

  T 'I 'False

(plus a coercion), which is ill-kinded.

comment:4 Changed 17 months ago by goldfire

#12102 is unrelated, I think.

comment:5 Changed 17 months ago by int-index

Cc: int-index added

comment:6 Changed 6 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:7 Changed 6 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T13643
Note: See TracTickets for help on using tickets.