cur-type-check? not behaving as expected

Question

cur-type-check? not behaving as expected

Closed this issue 4 years ago · 3 comments

#lang cur

(begin-for-syntax 
  (require rackunit) 
  (check-true 
    (cur-type-check? 
      #`(lambda (A : Type) (a : A) a) 
      #`(Π (A : Type) (a : A) A))))

Note:

> (begin-for-syntax (displayln (cur-type-infer #`(lambda (A : Type) (a : A) a))))

#<syntax:reflection.rkt:191:7 (cur-Π (A : (cur-Type 0)) (cur-Π (a : A) A))>

cur-type-check basically calls infer then type-check? in turnstile.

Answer 1 · 2020-06-17T21:54:42.000Z

It looks like cur-type-check? is not normalizing the expected type. It needs to call current-type-eval on the type there. (Looks like there used to be a call to cur-expand, but it got commented out at some point?)

Btw, in general I dont know how reliable curnel/reflection is. I didn't update it when I reimplemented the core, and I've actually been operating under the assumption that it's deprecated (I've been using turnstile libraries directly in my code).

I'm fine with bringing reflection back up to speed, but just be aware that it likely requires some more fixes (and tests!).

Answer 2 · 2020-06-17T21:56:07.000Z

Yeah it’s massively out of date. I’m going to patch some of it in the next few days, as much as I need to do my demo in this talk.

…

-- Sent from my phoneamajig

On Jun 17, 2020, at 14:54, Stephen Chang ***@***.***> wrote: It looks like cur-type-check? is not normalizing the expected type. It needs to call current-type-eval on the type there. (Looks like there used to be a call to cur-expand, but it got commented out at some point?) Btw, in general I dont know how reliable curnel/reflection is. I didn't update it when I reimplemented the core, and I've actually been operating under the assumption that it's deprecated (I've been using turnstile libraries directly in my code). I'm fine with bringing reflection back up to speed, but just be aware that it likely requires some more fixes (and tests!). — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe.

Answer 3 · 2020-06-17T22:04:42.000Z

Ah I see. Keep filing issues and I'll try to respond quickly.