motive arg for `new-elim` (and `elim`) doesnt do anything?
Closed this issue · 2 comments
stchang commented
Should the following program produce a type error, because the body of the motive doesnt match the branches? It actually doesnt seem to matter what I use as the motive at all. (elim also has the same behavior.)
#lang cur
(data Nat2 : 0 (Type 0)
(zz : Nat2)
(ss : (Π (n : Nat2) Nat2)))
(data Nat3 : 0 (Type 0)
(zzz : Nat3)
(sss : (Π (n : Nat3) Nat3)))
;; convert Nat2 to Nat3
(new-elim (ss (ss zz))
(λ (x : Nat2) Nat2)
zzz
(λ (n : Nat2) (λ (IH : Nat3) (sss IH))))
; => (sss (sss (zzz)))wilbowma commented
That's odd. It certainly should be a type error.
I'll look into this.
…On Tue, Aug 15, 2017 at 10:07:48AM -0700, Stephen Chang wrote:
Should the following program produce a type error, because the body of the motive doesnt match the branches? It actually doesnt seem to matter what I use as the motive at all. (`elim` also has the same behavior.)
```racket
#lang cur
(data Nat2 : 0 (Type 0)
(zz : Nat2)
(ss : (Π (n : Nat2) Nat2)))
(data Nat3 : 0 (Type 0)
(zzz : Nat3)
(sss : (Π (n : Nat3) Nat3)))
;; convert Nat2 to Nat3
(new-elim (ss (ss zz))
(λ (x : Nat2) Nat2)
zzz
(λ (n : Nat2) (λ (IH : Nat3) (sss IH))))
; => (sss (sss (zzz)))
```
--
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub:
#67
wilbowma commented
Okay I pushed a fix.
It looks like a change I made a while back introduced this bug, which dropped some failure
continuations responsible for reporting type errors.
The default to returned #f, but it used for a side effect in checking new-elim and got ignored.
I'll close this once I add a test case to the test suite.
…On Tue, Aug 15, 2017 at 10:07:48AM -0700, Stephen Chang wrote:
Should the following program produce a type error, because the body of the motive doesnt match the branches? It actually doesnt seem to matter what I use as the motive at all. (`elim` also has the same behavior.)
```racket
#lang cur
(data Nat2 : 0 (Type 0)
(zz : Nat2)
(ss : (Π (n : Nat2) Nat2)))
(data Nat3 : 0 (Type 0)
(zzz : Nat3)
(sss : (Π (n : Nat3) Nat3)))
;; convert Nat2 to Nat3
(new-elim (ss (ss zz))
(λ (x : Nat2) Nat2)
zzz
(λ (n : Nat2) (λ (IH : Nat3) (sss IH))))
; => (sss (sss (zzz)))
```
--
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub:
#67