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 <[email protected]> > Can you give an example of what you’d like to write, but can’t? > > Simon > > > > *From:* [email protected] [mailto: > [email protected]] *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 [email protected]] > > 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 <[email protected]> > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell > > >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
