Opened 5 months ago

Last modified 5 months ago

#13643 new bug

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:
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 5 months ago.

Download all attachments as: .zip

Change History (6)

Changed 5 months ago by Iceland_jack

Attachment: tPb2.log added

comment:1 Changed 5 months ago by Iceland_jack

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

#12102 is unrelated, I think.

comment:5 Changed 5 months ago by int-index

Cc: int-index added
Note: See TracTickets for help on using tickets.