| {-# LANGUAGE TypeFamilies #-}
|
| type family F a
|
| foo :: F a
| foo = undefined
|
| bar :: F a
| bar = foo
There is a real difficulty here with type-checking 'bar'. (And that difficulty
is why 'foo' is also rejected.)
Namely, when typechecking 'bar', we must instantiate
There is a real difficulty here with type-checking 'bar'. (And that
difficulty is why 'foo' is also rejected.)
Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1
installation doesn't complain. -- Conal
On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
Thanks, Jake! This suggestion helped a lot. -- Conal
On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur jake.mcart...@gmail.comwrote:
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type
Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1
installation doesn't complain. -- Conal
Yes, it is rejected.
Simon
From: conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] On Behalf Of
Conal Elliott
Sent: 14 January 2013 20:52
To: Simon Peyton-Jones
Cc:
I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE
Hello Conal,
The issue with your example is that it is ambiguous, so GHC can't figure
out how to instantiate the use of `foo`. It might be easier to see why
this is if you write it in this form:
foo :: (F a ~ b) = b
foo = ...
Now, we can see that only `b` appears on the RHS of the `=`, so
Hi Iavor,
Thanks for the remarks.
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
(forall a'. F a')`?
-- Conal
Hi Christian,
Given bar :: Bool, I can't see how one could go from Bool to F a =
Bool and determine a uniquely.
The same question applies to foo :: Bool, right? Yet no error message
there.
Regards, - Conal
On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen
Hello,
On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net wrote:
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type family F a
foo :: Tagged a (F a)
foo = Tagged undefined
bar :: Tagged a (F a)
bar = foo
This allows you to use the same newtype wrapper
On 1/13/13 3:52 PM, Iavor Diatchki wrote:
On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net wrote:
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this
11 matches
Mail list logo
