GitLab

For the implementation of fixpoint recursive definitions for a datatype I have defined the family:

type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One

for which we can define functor instances

instance (Functor (F [a])) where
   fmap _ (Left _) = Left ()
   fmap f (Right (a,x)) = Right (a,f x)
...

However, in the definition of recursive patterns over these representation, I need some coercions to hold such as

F d c ~  F a (c,a)

but in the current implementation they are evaluated as

F d ~ F a /\ c ~(c,a)

what does not express the semantics of "fully parameterized equality" that I was expecting

You can find a pratical example in (my conversions at the haskell-cafe mailing list)

In order to avoid this, the family could be redefined as

type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x

but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.

PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.

Trac metadata

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