[Template-haskell] Internal type consistency of quoted expressions

[Liyang HU]

(oops. Sorry about the double-post. Sent it with a wrong From: line
and it doesn't seem to have come through...)

Hello all,

Long story, but one thing after another led me to resort to TH as a
means to (re-)implement Conor McBride's (applicative) idiom
brackets[0], where:

   [[ g x0 x1 ... xn ]]    expands to    pure g <*> x0 <*> x1 <*> ... <*> xn

(pure and <*> come from Control.Applicative.)

While I can't use [[ and ]], I can define a CPP macro:

   #define II(e) $( idiom [| e |] )

where the idiom function does the above rewriting at compile time.
II( ... ) looks acceptable as a replacement for [[ ... ]]. Good. (Just as
well, since the type-level implementation of the iI Ii brackets given
in [1] will no longer work as of GHC 6.5, but is used fairly
extensively in the Epigram 2 source code...)

Even though (g x0 x1 ... xn) won't typecheck outside of a quotation, I
can nevertheless get away with [| g x0 x1 ... xn |] because it is
/internally/ consistent. (Template Meta-programming for Haskell, §7.1
paragraph 3; figure 2, rule BRACKET.)


Yesterday, Conor pointed out that the if and case constructs are pure
'things', and since my implementation of the above idiom function
seemed capable of this sort of syntax mangling, why not treat them as
one more case in the applicative/monadic idiom bracket. (I've always
wanted monadic if and case expressions. Hurrah!) The idea being that:

   II( if c then t else e )    and    II( case d of { ... } )

would expand to

   c >>= \ b -> if b then t else e
and
   d >>= \ x -> case x of { ... }

respectively. I'd already written some of this up, and just got around
to implementing the changes earlier tonight, but I'm stumped by the
internal type consistency restriction: c has type (Monad m => m Bool),
which means [| if c then t else e |] isn't 'internally consistent'.
With the case-expression, d has type (Monad m => m a); (x :: a); and
the elided patterns in { ... } match values of type a. So [| case d of
{ ... } |] won't get past the supposed 'sanity check'[2] either. :(


My current want-it-now 'solution' is to comment out the sole
tcSimplifyBracket invocation in ghc/compiler/typecheck/TcSplice.lhs.
Clearly this is the wrong approach, seeing as other people would like
to use this too. (I presume this will do what I want. I'm still
waiting for stage1 to finish building...)

I guess a more constructive approach would be to hack in an
alternative unchecked quotation bracket, [s| ... |] say ('s' stands
for 'syntax'). If upstream is willing to consider such an extension,
I'll get started...

Any alternative suggestions before I do? :-/

Thanks for listening,
/Liyang

[0] http://cs.nott.ac.uk/~ctm/IdiomLite.pdf
[1] http://cs.nott.ac.uk/~ctm/Idiom.pdf
[2] I am sane, right? I mean, is there any other reason for the
internal type-consistency check other than to detect /potential/
errors /earlier/?