*Main> let ty = polytype $ TForall (TypeVar "a") (TFun (tvar "a") (tvar "a"))
*Main> run (EAbs x (EApp (EAnno (EVar x) ty) (EVar x)))
"typesynth([], λx. (x : ∀ a. a → a) x)
typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], ($a : ∀ a. a → a) $a, ∃ 'b)
typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], ($a : ∀ a. a → a) $a)
typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], $a : ∀ a. a → a)
typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], $a, ∀ a. a → a)
typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], $a, 'c → 'c)
typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], $a)
=(∃ 'a, [▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c])
subtype([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], ∃ 'a, 'c → 'c)
instantiateL([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], 'a, 'c → 'c)
instantiateR([▶ 'a, ∃ 'e, ∃ 'd, ∃ 'a = ∃ 'd → ∃ 'e, ∃ 'b, $a : ∃ 'a, 'c], 'c, 'd)
*** Exception: The impossible happened! instantiateR: ([▶ 'a, ∃ 'e, ∃ 'd, ∃ 'a = ∃ 'd → ∃ 'e, ∃ 'b, $a : ∃ 'a, 'c], 'c, 'd)
*Main>