Re: [Haskell] Polymorphic types in RHS of type instances

Hi Simon, For instance: data Su n

data Fin n where FSu :: Fin n -> Fin (Su n) -- equivalent to data Fin n = forall m. n ~ Su m => FSu (Fin m)

data a :=: b where Refl :: a :=: a

type instance Rep (Fin n) = forall m. (n :=: Su m, Fin m)

But I think I found the answer in the meantime: this would quickly leave GHC trying to prove things such as (forall m. ... ~ forall m1. ...), which I guess is undecidable in general. Cheers, Pedro 2011/4/4 Simon Peyton-Jones

Can you give an example of what you’d like to write, but can’t?

Simon

*From:* glasgow-haskell-users-bounces@haskell.org [mailto: glasgow-haskell-users-bounces@haskell.org] *On Behalf Of *José Pedro Magalhães *Sent:* 04 April 2011 10:53 *To:* GHC users *Cc:* Steven Keuchel *Subject:* Re: [Haskell] Polymorphic types in RHS of type instances

Hi,

[Moving to glasgow-haskell-users@haskell.org]

I would also like to know the answer to this question. While I can imagine it has something to do with type checking/inference, it is not immediately clear to me where the problem lies.

Thanks, Pedro

On Sat, Feb 5, 2011 at 12:25, Steven Keuchel wrote:

Hi list,

I was wondering why GHC doesn't allow usage of polymorphic types in the right-hand side of type instance declarations for type families. The GHC user guide states: "The right-hand side of a type instance must be a monotype (i.e., it may not include foralls) [...]", but it doesn't state the reason.

I stumbled upon this limitation when I was trying to generically calculate Johann's and Ghani's interpreter (transformers) for nested data types from their "Initial Algebra Semantics is Enough!" paper.

Cheers, Steven

_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell