Core lint error with data families and promotion across modules

I have these files:

{-# LANGUAGE GADTs, PolyKinds, DataKinds, TypeFamilies #-}

module A where

data family SList (a :: k)
data instance SList (a :: [k]) where
  SNil :: SList '[]

module B where

import A

foo = SNil

If I compile them together, with -dcore-lint on, all is well. But, if I compile A and then B (both with -dcore-lint), I get this:

*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: Warning:
    In the type ‛A.SList '[]’
    Kind application error in type ‛[*]’
      Function kind = * -> *
      Arg kinds = [(*, BOX)]
<no location info>: Warning:
    In the type ‛A.SList '[]’
    Kind application error in type ‛A.SList '[]’
      Function kind = k_izi -> *
      Arg kinds = [([*], *), ('[], [*])]
*** Offending Program ***
B.foo :: A.SList '[]
[LclIdX, Str=DmdType]
B.foo = A.$WSNil @ *

*** End of Offense ***


<no location info>: 
Compilation had errors

This was tested on a very recent HEAD (Oct 11). The error does not happen if SList is a normal datatype, as opposed to a data family.

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture