Dependent type families cannot be separated from their instances
Summary
I'm doing experiments with some very dependently typed type families. It works all nice when everything is in a single file, but not when trying to split it into different modules.
Steps to reproduce
Minimal example: two type families F and G, where G's second argument depends on the first, and one instance for each family.
{-# LANGUAGE TypeFamilies #-}
module A where
import Data.Kind (Type)
type family F (x :: Type) :: Type
type family G (x :: Type) (y :: F x) :: Type
type instance F () = Type
type instance G () k = k
That compiles (tried on GHC 9.4). But if we move the last two lines to another module, we get:
B.hs:9:20: error:
• Expected kind ‘F ()’, but ‘k’ has kind ‘*’
• In the second argument of ‘G’, namely ‘k’
In the type instance declaration for ‘G’
|
9 | type instance G () k = k
|
If we then move the last line to yet another module, it compiles again.
It seems that when typechecking the G instance, GHC somehow does not see F's instance.
Even more weirdness: this behavior is not stable under expansion/folding of type synonyms.
The following refactoring of the instances does compile when separated from the family declarations:
type W = ()
type instance F () = Type
type instance G W k = k
(And other combinations of W and () don't compile.)
Expected behavior
These declarations should compile regardless of whether they are in separate files.
Environment
- GHC version used: 9.0, 9.2, 9.4