On 26/05/07, Dominic Steinitz
This seems even worse to me. A is not inhabited so how can 42 be of type A?
I think it should work. The context on the F constructor says that A is an instance of Num, so you could only have an F value if you could prove that A was an instance of Num. Therefore, when deconstructing in bar's pattern, if you match an F, then A must be an instance of Num, so to say 42 :: A is valid. F is a proof, or witness, of A's instantiation of Num. As A isn't, in actuality, an instance of Num, you can never have an F value, but that doesn't matter: all that bar does is express the fact that _if_ you have a value F, then it's valid to say 42 :: A. In a way, it's a bit like saying the following is a true statement: If there are 8 days in the week, then pigs can fly. Neither of the substatements ("there are 8 days in the week" and "pigs can fly"), when taken by themselves, are true. However, the statement as a whole is true. Here are a couple of ways of explaining this: * If you can prove that there are in fact 8 days in the week, then you must have a faulty logic system, so you could prove anything (including "pigs can fly"). * In order to disprove the statement, you'd have to prove that "there are 8 days in the week" is true and simultaneously that "pigs can fly is false". However, you can't do this, because you could never prove that "there are 8 days in the week" is true. Hence, the statement can't be false, so it must be true. (I'm ignoring the difference between truth and provability; think of my arguments as classical rather than intuitionistic.) -- -David House, dmhouse@gmail.com