Really cool sub-thread on why unification in dependently typed programming languages is hard, and what might trip up the unprepared language implementer!
Quote Tweet
Replying to @brendanzab @ireneista and 3 others
So e.g.:
const : a -> b -> a
const a _ = a
is implicitly quantifying over the types a and b. writing {…} for implicit bits, and ? for the bits we don’t know syntactically, we get:
const : {a : ?} -> {b : ?} -> a -> b -> a
const {_} {_} a _ = a