motoko-san: Let-bound variants

This change fixes the Viper translation of let-bound variants by
removing normalization from `infer_exp` in `typing.ml`, thus making the
nominal type accessible in `trans.ml`

src/mo_frontend/typing.ml

@@ -1115,7 +1115,7 @@ and infer_exp' f env exp : T.typ =
   if not env.pre then begin
     assert (T.normalize t' <> T.Pre);
     let e = A.infer_effect_exp exp in
-    exp.note <- {note_typ = T.normalize t'; note_eff = e}
+    exp.note <- {note_typ = t'; note_eff = e}
   end;
   t'
 

test/viper/ok/variants.tc.ok

@@ -0,0 +1 @@
+variants.mo:12.16-12.21: warning [M0194], unused identifier getBW (delete or rename to wildcard `_` or `_getBW`)

test/viper/ok/variants.vpr.ok

@@ -95,6 +95,16 @@ adt BW  { Black()
 adt Pair [A, B]
   { ordered(ordered$0 : A, ordered$1 : B)
     swapped(swapped$0 : Pair[B, A]) }
+method getBW($Self: Ref)
+     returns ($Res: BW)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var x: BW
+      x := Black();
+      $Res := x;
+      goto $Ret;
+      label $Ret; 
+    }
 method get($Self: Ref)
      returns ($Res: Pair[Int, BW])
     requires $Perm($Self)

test/viper/ok/variants.vpr.stderr.ok

@@ -0,0 +1 @@
+variants.mo:12.16-12.21: warning [M0194], unused identifier getBW (delete or rename to wildcard `_` or `_getBW`)

test/viper/variants.mo

@@ -9,6 +9,11 @@ actor Variants {
     #swapped : Pair<B, A>;
   };
 
+  private func getBW(): BW {
+    let x : BW = #Black;
+    return x;
+  };
+
   func idPair<A, B>(p: Pair<A, B>) : Pair<A, B> {
     return p;
   };