-
chevalier@alum.wellesley.edu authored
The way that newtype declarations were printed in External Core files was incomplete, since there was no declaration for the coercion introduced by a newtype. For example, the Haskell source: newtype T a = MkT (a -> a) foo (MkT x) = x got printed out in External Core as (roughly): %newtype T a = a -> a; foo :: %forall t . T t -> t -> t = %cast (\ @ t -> a1 @ t) (%forall t . T t -> ZCCoT t); There is no declaration anywhere in the External Core program for :CoT, so that's bad. I changed the newtype decl syntax so as to include the declaration for the coercion axiom introduced by the newtype. Now, it looks like: %newtype T a ^ (ZCCoT :: ((T a) :=: (a -> a))) = a -> a; And an external typechecker could conceivably typecheck code that uses this. The major changes are to MkExternalCore and PprExternalCore (as well as ExternalCore, to change the External Core AST.) I also corrected some typos in comments in other files. Documentation and external tool changes to follow.
2fbab1a0