Typing of Error ignores the type annotation on it, so big-step is type-preserving

[jaccokrijnen]

The Error t term is annotated with its type t. Therefore, typing could simply be

normalise T Tn ->
Delta ,, Gamma |-+ Error T : Tn

However, this does not suffice for type preservation, Joris' thesis section 4.2.7, "Error": in the eval big-step relation, the annotation is supposedly not enough to determine the annotation on the result error where errors are propagated (e.g. Apply (Error T1) (Error T2) ==> Error ?? . Effectively, the big-step semantics need to be aware of the type of the expression it is evaluating.

I think this could be solved by eval only evaluating well-typed terms, so there is no question about the resulting annotation on Error.

So instead, the typing rule is currently:

  | T_Error : forall Delta Gamma S T Tn,                                                                                                                                                                                                                                        
      Delta |-* T : Kind_Base ->      
      normalise T Tn ->        
      Delta ,, Gamma |-+ (Error S) : Tn

which ignores the annotation. And the big-step rules then trivially preserve typing (with a non-sensical annotation)

...
  | E_Error_Apply1 : forall t1 t2 j1 T,_
      t1 =[j1]=> Error T ->
      Apply t1 t2 =[j1 + 1]=> Error T
...

[jaccokrijnen]

Why are annotations on Error necessary in the first place? According to Manuel they are needed for having the principal type property while retaining a simple inference algorithm (reference: Practical Foundations Programming Languages (Harper))