mbenke / hm-typecheck

Experimental typechecker for a Solidity intermediate language
3 stars 1 forks source link

Typechecking annotates some variables incorrectly #2

Closed mbenke closed 4 months ago

mbenke commented 4 months ago
examples/mona/03option.fun
type Option[a] = None | Some[a];
just x = Some x;
maybe n o = case o of { None -> n; Some x -> x };
main = maybe 0 (just 42);

Typechecked program:
Option[a] = None  | Some a;
just (x:b) = (Some: b -> Option[b]) (x: b);
maybe (n:d1) (o:Option[d1]) = case<d1> (o: Option[d1]) of {
  None  -> (n: u);
  Some x -> (x: d1)
};

------------
Specialised:
------------
just$Int = \(x:Int) -> (Some$Int: Int -> Option[Int]) (x: Int)
main = (maybe$Int: Int -> Option[Int] -> Int) 0 ((just$Int: Int -> Option[Int]) 42)
maybe$Int = \(n:Int) (o:Option[Int]) -> case<Int> (o: Option[Int]) : Option[Int] of {
  None  -> (n: u);
  Some (x:Int) -> (x: d1)
}

In typechecked program we should have None -> (n: d1) instead of None -> (n: u)

in specialised version we should have

  None  -> (n: Int);
  Some (x:Int) -> (x: Int)