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 |