Type family with dodgy binding site leads to Core Lint error
The following program produces a Core Lint error on GHC 8.0 through HEAD:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family ConstType (a :: Type) :: Type where
ConstType _ = Type
type family F (x :: ConstType a) :: Type where
F (x :: ConstType a) = a
f :: F Int
f = let x = x in x
$ /opt/ghc/8.6.5/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the expression: x_aVX @ a1_aVT
@ a1_aVT is out of scope
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
f :: forall a. F (Int |> Sym (D:R:ConstType[0] <a>_N))
[LclIdX]
f = \ (@ a_a17q) ->
letrec {
x_aVX :: forall t. t
[LclId]
x_aVX
= \ (@ t_a17t) ->
letrec {
x_a17u :: t_a17t
[LclId]
x_a17u = x_a17u; } in
x_a17u; } in
(x_aVX @ a1_aVT)
`cast` (Sub (Sym (D:R:F[0] <a1_aVT>_N <a_a17q>_N <Int>_N))
:: a1_aVT
~R# F (Int |> Sym (D:R:ConstType[0] <a1_aVT>_N) ; (D:R:ConstType[0]
<a1_aVT>_N ; Sym (D:R:ConstType[0]
<a_a17q>_N))))
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
This is likely due to the way F
is defined, since F (x :: ConstType a) = a
expands to F (x :: Type) = a
, which is ill scoped.
Note that GHC is smart enough to catch this if ConstType
is defined as a type synonym. That is to say, GHC will simply error if you instead try feeding it this program:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type ConstType (a :: Type) = Type
type family F (x :: ConstType a) :: Type where
F (x :: ConstType a) = a
f :: F Int
f = let x = x in x
$ /opt/ghc/8.6.5/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:3: error:
• Family instance purports to bind type variable ‘a1’
but the real LHS (expanding synonyms) is: F x = ...
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’
|
10 | F (x :: ConstType a) = a
| ^^^^^^^^^^^^^^^^^^^^^^^^