Gradual-Typing / Grift

A compiler for the gradually typed lambda calculus
MIT License
76 stars 11 forks source link

Type-based-casts and coercions are not equivalent #81

Open LuKuangChen opened 5 years ago

LuKuangChen commented 5 years ago

The blame labels are different.

$ grift --type-based-casts p1.grift 
$ ./a.out 
Implicit cast in ascription on expression at p1.grift:2:2
$ grift --coercions p1.grift 
$ ./a.out 
Implicit cast in ascription on expression at p1.grift:1:1

Here is the content of p1.grift

((ann
  (ann
   (ann
    (lambda ([x : (Tuple Int Int)]) x)
    ((Tuple Int Int) -> (Tuple Dyn Dyn)))
   ((Tuple Int Int) -> (Tuple Dyn Bool)))
  ((Tuple Int Int) -> (Tuple Bool Bool)))
 (tuple 1 2))
akuhlens commented 5 years ago

This seems like a fundamental problem with the way tuple coercions are currently implemented. Good to know! We will need to talk about this on Tuesday.