diff --git a/tests/error-messages/ExpectFailure.fst.json_output.expected b/tests/error-messages/ExpectFailure.fst.json_output.expected
index dd69a2e413b..708f065563f 100644
--- a/tests/error-messages/ExpectFailure.fst.json_output.expected
+++ b/tests/error-messages/ExpectFailure.fst.json_output.expected
@@ -1,8 +1,8 @@
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":15},"end_pos":{"line":28,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":8},"end_pos":{"line":28,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
@@ -11,11 +11,11 @@
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":15},"end_pos":{"line":30,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":8},"end_pos":{"line":30,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> Got issues: [
-{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
+{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.Type.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
diff --git a/tests/error-messages/ExpectFailure.fst.output.expected b/tests/error-messages/ExpectFailure.fst.output.expected
index 58e223f85ce..b870eb71ec1 100644
--- a/tests/error-messages/ExpectFailure.fst.output.expected
+++ b/tests/error-messages/ExpectFailure.fst.output.expected
@@ -2,14 +2,14 @@
 * Error 189 at ExpectFailure.fst(20,12-20,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(24,12-24,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
@@ -32,20 +32,20 @@
 * Error 189 at ExpectFailure.fst(43,12-43,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(50,12-50,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(61,12-61,15):
   - Expected expression of type Prims.int
     got expression 'a'
-    of type FStar.Char.char
+    of type FStar.Char.Type.char
 
 >>]