[Haskell] Polymorphic types in RHS of type instances

[José Pedro Magalhães]

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 <simonpj at microsoft.com>

>  Can you give an example of what you’d like to write, but can’t?
>
> Simon
>
>
>
> *From:* glasgow-haskell-users-bounces at haskell.org [mailto:
> glasgow-haskell-users-bounces at 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 at 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 <steven.keuchel at gmail.com>
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110404/4d9912f7/attachment.htm>