Preserve type annotations during normalization (#382)

* Add regression test

* Preserve type annotations during normalization

* Add regression test for annotations occuring in neutral expressions

* Fix pretty-printing annotations

* Add neutral type annotations

* Improve comments

* Make codecov purely informational on patches

codecov.yml

@@ -2,4 +2,7 @@ coverage:
   status:
     project:
       default:   # default is the status check's name, not default settings
-        informational: true
+        informational: true
+    patch:
+      default:
+        informational: true

lang/ast/src/exp/anno.rs

@@ -82,7 +82,7 @@ impl Print for Anno {
         _prec: Precedence,
     ) -> Builder<'a> {
         let Anno { exp, typ, .. } = self;
-        exp.print(cfg, alloc).parens().append(COLON).append(typ.print(cfg, alloc))
+        exp.print(cfg, alloc).append(COLON).append(typ.print(cfg, alloc)).parens()
     }
 }
 

lang/elaborator/src/normalizer/env.rs

@@ -1,5 +1,3 @@
-use derivative::Derivative;
-
 use ast::{Shift, ShiftRange, VarBound};
 use pretty::DocAllocator;
 
@@ -12,8 +10,7 @@ use printer::Print;
 
 use crate::normalizer::val::*;
 
-#[derive(Debug, Clone, Derivative)]
-#[derivative(Eq, PartialEq, Hash)]
+#[derive(Debug, Clone)]
 pub struct Env {
     /// Environment for locally bound variables
     bound_vars: GenericCtx<Box<Val>>,

lang/elaborator/src/normalizer/eval.rs

@@ -4,13 +4,16 @@ use log::trace;
 
 use ast::ctx::{BindContext, Context};
 use ast::*;
+use miette_util::ToMiette;
 use printer::types::Print;
 
 use crate::normalizer::env::*;
 use crate::normalizer::val::{self, Closure, Val};
 
 use crate::{result::*, TypeInfoTable};
 
+use super::val::AnnoNeu;
+
 pub trait Eval {
     type Val;
 
@@ -129,7 +132,11 @@ impl Eval for DotCall {
         let exp = exp.eval(info_table, env)?;
         let args = args.eval(info_table, env)?;
 
-        match (*exp).clone() {
+        // If possible, strip away all annotations from the expression.
+        // For example, we need to strip away the annotation around `T` in  `(T : Bool).match { T => F, F => T }` before we can evaluate further.
+        let exp = strip_annotations(&exp);
+
+        match exp {
             Val::Call(val::Call { name: call_name, kind, args: call_args, .. }) => {
                 match kind {
                     CallKind::Constructor => {
@@ -224,6 +231,7 @@ impl Eval for DotCall {
                 // Then we apply the body to the `args`.
                 body.clone().unwrap().apply(info_table, &args.to_vals())
             }
+
             Val::Neu(exp) => {
                 // The specific instance of the DotCall we are evaluating is:
                 //
@@ -246,17 +254,46 @@ impl Eval for DotCall {
                     .into(),
                 )))
             }
-            _ => unreachable!(),
+            Val::Anno(_) => Err(TypeError::Impossible {
+                message: "Type annotation was not stripped when evaluating DotCall".to_owned(),
+                span: span.to_miette(),
+            }),
+            Val::TypCtor(_) => Err(TypeError::Impossible {
+                message: "Cannot apply DotCall to type constructor".to_owned(),
+                span: span.to_miette(),
+            }),
+            Val::TypeUniv(_) => Err(TypeError::Impossible {
+                message: "Cannot apply DotCall to type universe".to_owned(),
+                span: span.to_miette(),
+            }),
         }
     }
 }
 
+/// Given a value, strip away all the annotations and return the inner value.
+/// Unless the inner value is neutral, in which case all annotations become neutral.
+/// For example, stripping the annotations from `((T : Bool): Bool)` would yield `T` because `T` is not neutral.
+/// Stripping the annotations from `((x: Bool): Bool)` would yield `((x: Bool): Bool)` because `x` is neutral.
+fn strip_annotations(val: &Val) -> Val {
+    match val {
+        Val::Anno(anno) => match strip_annotations(&anno.exp) {
+            Val::Neu(neu) => Val::Neu(
+                AnnoNeu { span: anno.span, exp: Box::new(neu), typ: anno.typ.clone() }.into(),
+            ),
+            val => val,
+        },
+        val => val.clone(),
+    }
+}
+
 impl Eval for Anno {
     type Val = Box<Val>;
 
     fn eval(&self, info_table: &Rc<TypeInfoTable>, env: &mut Env) -> Result<Self::Val, TypeError> {
-        let Anno { exp, .. } = self;
-        exp.eval(info_table, env)
+        let Anno { span, exp, typ, normalized_type: _ } = self;
+        let exp = exp.eval(info_table, env)?;
+        let typ = typ.eval(info_table, env)?;
+        Ok(Box::new(val::AnnoVal { span: *span, exp, typ }.into()))
     }
 }
 
@@ -290,7 +327,9 @@ impl Eval for LocalMatch {
         let on_exp = on_exp.eval(info_table, env)?;
         let cases = cases.eval(info_table, env)?;
 
-        match (*on_exp).clone() {
+        let on_exp = strip_annotations(&on_exp);
+
+        match on_exp {
             Val::Call(val::Call { name: ctor_name, args, .. }) => {
                 // The specific instance of the LocalMatch we are evaluating is:
                 //
@@ -334,7 +373,22 @@ impl Eval for LocalMatch {
                     .into(),
                 )))
             }
-            _ => unreachable!(),
+            Val::TypCtor(typ_ctor) => Err(TypeError::Impossible {
+                message: "Cannot match on a type constructor".to_owned(),
+                span: typ_ctor.span.to_miette(),
+            }),
+            Val::TypeUniv(type_univ) => Err(TypeError::Impossible {
+                message: "Cannot match on a type universe".to_owned(),
+                span: type_univ.span.to_miette(),
+            }),
+            Val::LocalComatch(local_comatch) => Err(TypeError::Impossible {
+                message: "Cannot match on a local comatch".to_owned(),
+                span: local_comatch.span.to_miette(),
+            }),
+            Val::Anno(anno_val) => Err(TypeError::Impossible {
+                message: "Type annotation was not stripped when evaluating local match".to_owned(),
+                span: anno_val.span.to_miette(),
+            }),
         }
     }
 }