Closed type family declarations in hs-boots
Summary
A.hs-boot:
module A where
type A :: * -> *
type family A x
A.hs
module A where
type A :: * -> *
type family A x where
A () = ()
Then run
ghc -XTypeFamilies A.hs
It fails with:
[2 of 2] Compiling A ( A.hs, A.o )
A.hs:4:1: error:
Type constructor ‘A’ has conflicting definitions in the module
and its hs-boot file
Main module: type A :: * -> *
type family A x where
A () = ()
Boot file: type A :: * -> *
type family A x
|
4 | type family A x where
| ^^^^^^^^^^^^^^^^^^^^^...
Expected behavior
I would expect a forward declaration of the type family to work. Granted, it would never reduce without the actual module (ie if you had only a {-# SOURCE -#} import of A
), however, the inability to do this requires the full type family to be
In my interpretation of the type families section of the user guide, this is the advertised behaviour:
A closed type family may be declared with no equations. Such closed type families are opaque type-level definitions that will never reduce, are not necessarily injective (unlike empty data types), and cannot be given any instances. This is different from omitting the equations of a closed type family in a hs-boot file, which uses the syntax where .., as in that case there may or may not be equations given in the hs file.
Environment
- GHC version used: 9.4, 9.6, 9.8
Observations
This came up in the vulkan
library, which has a very large type family with a forward declaration in the hs-boot file.
This module, surprisingly, despite the "undefined" type family in the boot file, compiles with 9.8.1. It doesn't compile with 9.8.2 however (fails with the same error as the reproducer).
@phadej has reported that the reproducer above non-deterministically succeeds with 8.6