Re: Building on android - compiled program segfaults
Hi Nathan, On Fri, Jan 11, 2013 at 12:36 PM, Nathan Hüsken nathan.hues...@posteo.de wrote: I was succesfull in building ghc (pulled from git) to compile for arm-linux-androideabi! Great news! Can you describe how you managed to build it and which environment you use? main = putStrLn Hello, World I get an executable, which I can run on my android device. Unfortantly it segfaults. just a random idea, does main = error Hello, World work? Thanks, Bernhard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Building on android - compiled program segfaults
On 11 January 2013 19:36, Nathan Hüsken nathan.hues...@posteo.de wrote: Hi, I was succesfull in building ghc (pulled from git) to compile for arm-linux-androideabi! Now using inplace/bin/ghc-stage1 -dcore-lint -debug I compiler this Main.hs: main = putStrLn Hello, World I get an executable, which I can run on my android device. Unfortantly it segfaults. Running it with ./Main +RTS -DS gives: cap 0: initialised Now I am trying to debug this in gdb. When I try to display the stack (which should be in r13 on arm of I understand correctly, I get); (gdb) p8 $r13 0xbef00a74: 0x0 0xbef00a70: 0x0 0xbef00a6c: 0x3c2e74 0xbef00a68: 0x530350 0xbef00a64: 0x0 0xbef00a60: 0x0 0xbef00a5c: 0x0 0xbef00a58: 0x0 And now I am clueless. So I tried the good old printf debugging in the rts. Using this, I see that it gets before the call to scheduleWaitThread in the function rts_evalLazyIO (in RtsAPI.c). But when I put a printf in the beginning of scheduleWaitThread (in Schedule.c) it is not shown. What else can I do to find out more? can you strace it? Conrad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Building on android - compiled program segfaults
There is some more success :). When I do an unregisterised build, it works without segfault. On 01/13/2013 11:16 AM, Bernhard Urban wrote: Hi Nathan, On Fri, Jan 11, 2013 at 12:36 PM, Nathan Hüsken nathan.hues...@posteo.de wrote: I was succesfull in building ghc (pulled from git) to compile for arm-linux-androideabi! Great news! Can you describe how you managed to build it and which environment you use? I am on ubuntu 64 bit. I am planing to share the information in a blog post, but I will wait if I (or someone else) gets the registerised build to work. I made a short writedown of the steps it took here: https://github.com/RudolfVonKrugstein/jshaskell-blog/blob/master/android_ghc/android_ghc.md Regards, Nathan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Building on android - compiled program segfaults
Mmh, that does not seem to work. (gdb) strace warning: Couldn't determine the static tracepoint marker to probe Static tracepoint 1 at 0x3f0588 On 01/13/2013 12:56 PM, Conrad Parker wrote: On 11 January 2013 19:36, Nathan Hüsken nathan.hues...@posteo.de wrote: Hi, I was succesfull in building ghc (pulled from git) to compile for arm-linux-androideabi! Now using inplace/bin/ghc-stage1 -dcore-lint -debug I compiler this Main.hs: main = putStrLn Hello, World I get an executable, which I can run on my android device. Unfortantly it segfaults. Running it with ./Main +RTS -DS gives: cap 0: initialised Now I am trying to debug this in gdb. When I try to display the stack (which should be in r13 on arm of I understand correctly, I get); (gdb) p8 $r13 0xbef00a74: 0x0 0xbef00a70: 0x0 0xbef00a6c: 0x3c2e74 0xbef00a68: 0x530350 0xbef00a64: 0x0 0xbef00a60: 0x0 0xbef00a5c: 0x0 0xbef00a58: 0x0 And now I am clueless. So I tried the good old printf debugging in the rts. Using this, I see that it gets before the call to scheduleWaitThread in the function rts_evalLazyIO (in RtsAPI.c). But when I put a printf in the beginning of scheduleWaitThread (in Schedule.c) it is not shown. What else can I do to find out more? can you strace it? Conrad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Understand disassemble for segfault on android
Ok, the instruction
ldr r1, [r0, #140] - tso = CurrentTSO
seems the assume that REG_Base is r0 (140 is the offset of the tso in
StgRegTable, to which the REG_Base register should point).
But according to MachRegs.h on arm architecture, REG_Base should be r4.
Ineed, when I do
p *(unsigned int*)($r4+140)
I get (after converting to hex) is:
0x401033C0
looking at the backtrace:
(...)
#3 0x003c4cb0 in scheduleWaitThread (tso=0x401033c0, ret=0x0,
pcap=0xbe843b6c)
(...)
this is the same address as given to scheduleWaitThread for tso.
So the question is, why is r0 and not r4 used???
Regards,
Nathan
On 01/13/2013 12:10 AM, Nathan Hüsken wrote:
Hey,
I am still investigating the segfaults of the exectuable produced by ghc
to arm-linux-androideabi cross compiler.
I need help. Can someone tell me if my conclusions are correct?
The crash happens here:
Dump of assembler code for function stg_returnToStackTop:
0x003f059c +0: push{r4, lr}
0x003f05a0 +4: sub sp, sp, #16
0x003f05a4 +8: ldr r1, [r0, #140] ; 0x8c
= 0x003f05a8 +12: ldr r12, [r1, #12]
0x003f05ac +16: ldr r1, [r12, #12]
0x003f05b0 +20: mov r2, #0
Since it is in the begining of stg_returnToStackTop, it has to be
LOAD_THREAD_STATE();
I believe the code for this is produced by loadThreadState:
loadThreadState dflags tso stack = do
catAGraphs [
-- tso = CurrentTSO;
mkAssign (CmmLocal tso) stgCurrentTSO,
-- stack = tso-stackobj;
mkAssign (CmmLocal stack) (CmmLoad (cmmOffset dflags (CmmReg
(CmmLocal tso)) (tso_stackobj dflags)) (bWord dflags)),
(...)
So I believe the instruction are mapped like this:
ldr r1, [r0, #140] - tso = CurrentTSO
ldr r12, [r1, #12] - stack = tso-stackobj
If that is true, the loaded tso pointer ([r0, #140]) must be wrong.
When I look at the backtrace at the moment of crash:
#0 0x003f0588 in stg_returnToStackTop ()
#1 0x003c2e74 in schedule (initialCapability=0x3f057c, task=0x52f350)
at rts/Schedule.c:463
#2 0x003c2e74 in schedule (initialCapability=0x52f340, task=0x400a42f0)
at rts/Schedule.c:463
#3 0x003c4cb0 in scheduleWaitThread (tso=0x401033c0, ret=0x0,
pcap=0xbe843b6c)
at rts/Schedule.c:2351
There is a tso value passed to scheduleWaitThread (tso=0x401033c0).
Should be this is the same address, form where the tso is loaded in the
instruction:
ldr r1, [r0, #140] - tso = CurrentTSO
? If so, the value in r0 is way of.
info register
r0 0x3f057c 4130172
r1 0xe24dd010 -498216944
Are my conclusions so far correct, and I have to find out why r0 is
having the wrong value?
Thanks!
Nathan
___
ghc-devs mailing list
ghc-d...@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Building ghc on raspberry pi.
On Sun, 13 Jan 2013, Neil Davies wrote: Sounds like we're close - I must admit I've slightly lost track of the things that need to be done. Can we start collecting the pre-conditionds and steps, when each complete build takes best part of a day, its difficult to keep the context. So - taking the ghc 7.4.1 that is part of raspian wheezy (pkg version 7.4.1-4+rpi1) which depends upon (amongst others) llvm-3.0 (pkg version 3.0-10), can we capture the changes? Which version of LLVM is being used? I'm using LLVM 3.1 and gcc 4.6.3 and ghc 7.4.1. Which ghc source(s) are you starting from? ghc-7.6.1 with http://hackage.haskell.org/trac/ghc/attachment/ticket/5914/0001-add-support-for-ARM-hard-float-ABI-fixes-5914.patch applied, fixing the hunks in compiler/main/DriverPipeline.hs by hand. What files did you need to touch in the make process? Please supply diffs I've been fiddling with various parmameters in mk/build.mk. Anything else? I haven't got it compiling yet. Oh I'm currently using the raspian distriubtion with uses the hard-float ABI, but my end-goal is to bootstrap a nix package. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Building ghc on raspberry pi.
Understood I've got another RPi supposed to arrive this week - would more computation power help anyone out there? Neil On 13 Jan 2013, at 15:59, rocon...@theorem.ca wrote: On Sun, 13 Jan 2013, Neil Davies wrote: Sounds like we're close - I must admit I've slightly lost track of the things that need to be done. Can we start collecting the pre-conditionds and steps, when each complete build takes best part of a day, its difficult to keep the context. So - taking the ghc 7.4.1 that is part of raspian wheezy (pkg version 7.4.1-4+rpi1) which depends upon (amongst others) llvm-3.0 (pkg version 3.0-10), can we capture the changes? Which version of LLVM is being used? I'm using LLVM 3.1 and gcc 4.6.3 and ghc 7.4.1. Which ghc source(s) are you starting from? ghc-7.6.1 with http://hackage.haskell.org/trac/ghc/attachment/ticket/5914/0001-add-support-for-ARM-hard-float-ABI-fixes-5914.patch applied, fixing the hunks in compiler/main/DriverPipeline.hs by hand. What files did you need to touch in the make process? Please supply diffs I've been fiddling with various parmameters in mk/build.mk. Anything else? I haven't got it compiling yet. Oh I'm currently using the raspian distriubtion with uses the hard-float ABI, but my end-goal is to bootstrap a nix package. -- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Advice on type families and non-injectivity?
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
Hi,
How would you infer a from F a? Given bar :: Bool, I can't see how
one could go from Bool to F a = Bool and determine a uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 20:13]:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
pgpDSTt_twtD7.pgp
Description: PGP signature
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
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 there is
really no way for GHC to figure out what is the intended value for `a`.
Replacing `a` with a concrete type (such as `Bool`) eliminates the
problem, because now GHC does not need to come up with a value for `a`.
Another way to eliminate the ambiguity would be if `F` was injective---then
we'd know that `b` uniquely determines `a` so again there would be no
ambiguity.
If `F` is not injective, however, the only workaround would be to write the
type in such a way that the function arguments appear in the signature
directly (e.g., something like 'a - F a' would be ok).
-Iavor
On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott co...@conal.net wrote:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
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
On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki
iavor.diatc...@gmail.comwrote:
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 there is
really no way for GHC to figure out what is the intended value for `a`.
Replacing `a` with a concrete type (such as `Bool`) eliminates the
problem, because now GHC does not need to come up with a value for `a`.
Another way to eliminate the ambiguity would be if `F` was injective---then
we'd know that `b` uniquely determines `a` so again there would be no
ambiguity.
If `F` is not injective, however, the only workaround would be to write
the type in such a way that the function arguments appear in the signature
directly (e.g., something like 'a - F a' would be ok).
-Iavor
On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott co...@conal.net wrote:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
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
choe...@tbi.univie.ac.at wrote:
Hi,
How would you infer a from F a? Given bar :: Bool, I can't see how
one could go from Bool to F a = Bool and determine a uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 20:13]:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type
and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
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 `(forall a. F a) == (forall a'. F a')`? Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter? Anyway, if there was a way to assert something like that about a type-function, than there would be no problem. When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind. By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error). -Iavor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Bytestring and GHC 7.6.2
On 12 January 2013 16:05, Ian Lynagh i...@well-typed.com wrote: On Tue, Jan 08, 2013 at 08:10:18PM +, Duncan Coutts wrote: Either way, lemme know if this is all fine, and I'll make the 0.10.0.2 release. Looks good, thanks! I've updated the GHC 7.6 repo to match the tag. Ta muchly! ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
Hi Conal,
if you take your example program and write foo :: Bool, ghci accepts it?
For me it complains, and I would think rightly so, that couldn't match
expected type Fa with actual type Bool. It actually only works with the
following quite useless type instance F a = Bool.
By the way, using above instance, the original example works... ;-)
Ultimatively, injective type families would be useful. Thinking about
roman's vector library for example. For my code, I am switching more and
more to data families to get the desired behaviour of: F a ~ F b = a ~ b
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 21:14]:
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 Ho:ner zu Siederdissen
choe...@tbi.univie.ac.at wrote:
Hi,
How would you infer a from F a? Given bar :: Bool, I can't see how
one could go from Bool to F a = Bool and determine a uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 20:13]:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type
and
then compare with the given one? Or is there an issue even with
type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
pgpQQPvW8QNiU.pgp
Description: PGP signature
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on type families and non-injectivity?
Hi Conal,
I agree that your initial example is a little puzzling, and I'm glad that the
new ambiguity checker prevents both definitions, not just one.
However, your initial question seems broader than just this example. I have run
into this problem (wanting injective type functions) several times myself, and
have been successful at finding workarounds. But, I can't think of any unifying
principle or solid advice. If you can post more information about your problem,
perhaps I or others can contribute.
For what it's worth, the desire for injective type functions has been entered
as ticket #6018 in the GHC Trac, but I see you're already on the cc: list. I
believe Simon PJ has given serious thought to implementing this feature and may
have even put in some very basic code toward this end.
Richard
On Jan 13, 2013, at 2:10 PM, Conal Elliott co...@conal.net wrote:
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 TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and then
compare with the given one? Or is there an issue even with type *checking* in
such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the convenience
of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
