diff --git a/src/stages/5-ast_typed/PP_generic.ml b/src/stages/5-ast_typed/PP_generic.ml
index 1e503ace6..c29a31b30 100644
--- a/src/stages/5-ast_typed/PP_generic.ml
+++ b/src/stages/5-ast_typed/PP_generic.ml
@@ -89,7 +89,7 @@ module M = struct
       option = (fun _visitor continue NoState o ->
         match o with
         | None -> fprintf ppf "None"
-        | Some v -> fprintf ppf "%a" (fun _ppf -> continue NoState) v) ;
+        | Some v -> fprintf ppf "Some %a" (fun _ppf -> continue NoState) v) ;
       poly_unionfind            = (fun _visitor continue NoState p   ->
         let lst = (UnionFind.Poly2.partitions p) in
         let aux1 l = fprintf ppf "[@,@[<hv 2> (*%a*) %a @]@,]"
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index 389f93e89..da0bcdd50 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -230,9 +230,15 @@ module Substitution = struct
       | P_forall p -> (
           let aux c = constraint_ ~c ~substs in
           let constraints = List.map aux p.constraints in
-          if (p.binder = v) then (
+          if (Var.equal p.binder v) then (
+            (* The variable v is shadowed by the forall's binder, so
+               we don't substitute inside the body. This should be
+               handled in a more elegant manner once we have a proper
+               environment and scopes. *)
             { tsrc = "?TODO3?" ; t = P_forall { p with constraints } }
           ) else (
+            (* The variable v is still visible within the forall, so
+               substitute also within the body *)
             let body = self p.body in
             { tsrc = "?TODO4?" ; t = P_forall { p with constraints ; body } }
           )
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index 12ea7cc9c..9ed64a53c 100644
--- a/src/test/test_helpers.ml
+++ b/src/test/test_helpers.ml
@@ -99,7 +99,8 @@ let typed_program_with_imperative_input_to_michelson
   let%bind sugar            = Compile.Of_imperative.compile_expression input in
   let%bind core             = Compile.Of_sugar.compile_expression sugar in
   let%bind app              = Compile.Of_core.apply entry_point core in
-  let%bind (typed_app,_)    = Compile.Of_core.compile_expression ~env ~state app in
+  let%bind (typed_app,new_state)    = Compile.Of_core.compile_expression ~env ~state app in
+  let () = Typer.Solver.discard_state new_state in
   let%bind compiled_applied = Compile.Of_typed.compile_expression typed_app in
   let%bind mini_c_prg       = Compile.Of_typed.compile program in
   Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied