Type family signatures in indefinite modules

Backpack does not allow type family signatures in indefinite modules. As an example, although GHC does accept:

-- indefinite module
data Foo :: Bool
-- implementing module
type Foo = 'True

It does not accept:

-- indefinite module
type family Foo (b :: Bool) :: Bool
-- implementing module
type family Foo (b :: Bool) :: Bool where
  Foo 'True = 'False
  Foo 'False = 'True

I'm not sure if there is a fundamental reason for this (e.g. a requirement that everything is matchable). It would be helpful for the thing I'm experimenting with if this restriction could be lifted.

Trac metadata

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

changed weight to 5

added Tfeature request Trac import backpack labels

I've stumbled across some additional relevant information. GHC does allow closed type family declarations in hs-boot files. The syntax for doing this is bizarre:

type family Foo (a :: Bool) :: Type where ..

The two periods are actually used just like that. It's strange that since backpack reuses so much of what hs-boot files provide, it does not support type families as well.

This syntax also works in backpack files. I had made a typo when attempting to use it. Closing.

closed

added Pnormal label