modal types, generalized arrows, and core passes written in coq

[Adam Megacz]

Max Bolingbroke <batterseapower at hotmail.com> writes:
> ==================== Coq Pass Output ====================ghc-stage2:
> panic! (the 'impossible' happened)
>   (GHC version 7.1.20110308 for i386-apple-darwin):
> 	unable to convert HaskWeak to HaskStrong due to:\n  type mismatch in
> HaskWeak ELet: t and GHC.Types.Bool
>
> Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Did HelloWorld work?  See the commands here:

  http://www.cs.berkeley.edu/~megacz/garrows/

Also, you appear to be using -dcoqpass (right?) which you're not
supposed to use with the tutorial.  That flag builds proof-trees as
LaTeX code and unless you've recompiled it with expanded limits, LaTeX
will surely choke on anything as large asthe tutorial (it can just
barely handle "pow").

Regarding -fcoqpass, I hope to post that on Monday.  But in the meantime
everything else (principally type inference and checking) should work
just fine with -XModalTypes and no other special flags.  Please let me
know if you see otherwise.

Thanks!!

  - a