Open brianberns opened 1 year ago
For reference, here's an example where this problem occurs:
x -> x
and y -> Int
.x
and y
are unified, producing substitution x <- y
.x
and Int
, producing y
and Int
.y
and Int
are unified, producing substitution y <- Int
.x <- y, y <- Int
.One might argue instead that the composed substitution should be x <- Int
, but this is not the current behavior of the algorithm.
The
Substitutable
instance forType
is currently defined as follows:I believe the
TVar
case is incomplete. Consider the following substitution:If we apply this substitution to type variable
x
, we obtainy
, when we should obtainInt
. I think this case should instead recursively apply the substitution to the type found in the map.