`match` on `Bool` not same as `new-elim` with `Bool`

[stchang]

(may be related to #66?)

match with a Bool does not behave the same as new-elim with a Bool

#lang cur
(require cur/stdlib/prop
         cur/stdlib/sugar
         cur/stdlib/bool)
;; ok
(:: (λ [b : Bool]
      (new-elim b
                (λ [b : Bool] (== Bool (not (not b)) b))
                (refl Bool true)
                (refl Bool false)))
    (∀ [b : Bool] (== Bool (not (not b)) b)))

but:

(:: (λ [b : Bool]
      (match b #:in Bool #:return (== Bool (not (not b)) b)
        [true (refl Bool true)]
        [false (refl Bool false)]))
    (∀ [b : Bool] (== Bool (not (not b)) b)))

errors with:

core-type-error: Expected type (#%plain-app cur-elim (#%plain-app cur-elim b (#%plain-app cur-λ Bool (#%plain-lambda (anon-discriminant695) Bool)) false true) (#%plain-app cur-λ Bool (#%plain-lambda (anon-discriminant695) Bool)) false true), but found type true while checking method for true
  at: (#%plain-app cur-apply (#%plain-app cur-apply refl Bool) true)
  in: (#%plain-app cur-apply (#%plain-app cur-apply refl Bool) true)

[wilbowma]

Yeah. Declaring code backruptcy for the implementation of match.

[wilbowma]

wontfix until #55