Change syntax for newtypes in External Core

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.

diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs
index 7687317..9b67515 100644 (file)
--- a/compiler/coreSyn/CoreSyn.lhs
+++ b/compiler/coreSyn/CoreSyn.lhs
@@ -138,7 +138,7 @@ Invariant: The remaining cases are in order of increasing
 Invariant: The list of alternatives is ALWAYS EXHAUSTIVE,
           meaning that it covers all cases that can occur
 
-    An "exhausive" case does not necessarily mention all constructors:
+    An "exhaustive" case does not necessarily mention all constructors:
        data Foo = Red | Green | Blue
 
        ...case x of 

diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs
index 86a0d03..5754f84 100644 (file)
--- a/compiler/coreSyn/ExternalCore.lhs
+++ b/compiler/coreSyn/ExternalCore.lhs
@@ -10,12 +10,15 @@ data Module
 
 data Tdef 
   = Data (Qual Tcon) [Tbind] [Cdef]
-  | Newtype (Qual Tcon) [Tbind] (Maybe Ty)
+  | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty)
 
 data Cdef 
   = Constr Dcon [Tbind] [Ty]
   | GadtConstr Dcon Ty
 
+-- Newtype coercion
+type Axiom = (Qual Tcon, Kind)
+
 data Vdefg 
   = Rec [Vdef]
   | Nonrec Vdef

diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs
index c1e5217..1dc3b7e 100644 (file)
--- a/compiler/coreSyn/MkExternalCore.lhs
+++ b/compiler/coreSyn/MkExternalCore.lhs
@@ -61,9 +61,23 @@ collect_tdefs tcon tdefs
   | isAlgTyCon tcon = tdef: tdefs
   where
     tdef | isNewTyCon tcon = 
-                C.Newtype (make_con_qid (tyConName tcon)) (map make_tbind tyvars) repclause 
+                C.Newtype (qtc tcon) (map make_tbind tyvars) 
+                  (case newTyConCo_maybe tcon of
+                     Just coercion -> (qtc coercion, 
+                       make_kind $ (uncurry mkCoKind) $  
+                                  case isCoercionTyCon_maybe coercion of
+                                    -- See Note [Newtype coercions] in 
+                                    -- types/TyCon
+                                    Just (arity,coKindFun) -> coKindFun $
+                                       map mkTyVarTy $ take arity tyvars
+                                    Nothing -> pprPanic ("MkExternalCore:\
+                                      coercion tcon should have a kind fun")
+                                        (ppr tcon))
+                     Nothing       -> pprPanic ("MkExternalCore: newtype tcon\
+                                       should have a coercion: ") (ppr tcon))
+                   repclause 
          | otherwise = 
-                C.Data (make_con_qid (tyConName tcon)) (map make_tbind tyvars) (map make_cdef (tyConDataCons tcon)) 
+                C.Data (qtc tcon) (map make_tbind tyvars) (map make_cdef (tyConDataCons tcon)) 
          where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing
                         | otherwise = Just (make_ty (repType rhs))
                                            where (_, rhs) = newTyConRhs tcon
@@ -71,6 +85,9 @@ collect_tdefs tcon tdefs
 
 collect_tdefs _ tdefs = tdefs
 
+qtc :: TyCon -> C.Qual C.Tcon
+qtc = make_con_qid . tyConName
+
 
 make_cdef :: DataCon -> C.Cdef
 make_cdef dcon =  C.Constr dcon_name existentials tys
@@ -160,7 +177,7 @@ make_ty (TyVarTy tv)         = C.Tvar (make_var_id (tyVarName tv))
 make_ty (AppTy t1 t2)           = C.Tapp (make_ty t1) (make_ty t2)
 make_ty (FunTy t1 t2)           = make_ty (TyConApp funTyCon [t1,t2])
 make_ty (ForAllTy tv t)         = C.Tforall (make_tbind tv) (make_ty t)
-make_ty (TyConApp tc ts)        = foldl C.Tapp (C.Tcon (make_con_qid (tyConName tc))) 
+make_ty (TyConApp tc ts)        = foldl C.Tapp (C.Tcon (qtc tc)) 
                                         (map make_ty ts)
 -- Newtypes are treated just like any other type constructor; not expanded
 -- Reason: predTypeRep does substitution and, while substitution deals

diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs
index 6808144..22449df 100644 (file)
--- a/compiler/coreSyn/PprExternalCore.lhs
+++ b/compiler/coreSyn/PprExternalCore.lhs
@@ -5,11 +5,13 @@
 \begin{code}
 module PprExternalCore () where
 
-import Pretty
 import ExternalCore
-import Char
 import Encoding
 
+import Pretty
+import Char
+
+
 instance Show Module where
   showsPrec _ m = shows (pmodule m)
 
@@ -52,11 +54,20 @@ ptdef (Data tcon tbinds cdefs) =
   (text "%data" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> char '=')
   $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
 
-ptdef (Newtype tcon tbinds rep ) =
-  text "%newtype" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> repclause
-       where repclause = case rep of
-                           Just ty -> char '=' <+> pty ty 
-                          Nothing -> empty
+ptdef (Newtype tcon tbinds (coercion,k) rep) =
+-- Here we take apart the newtype tycon in order to get the newtype coercion,
+-- which needs to be represented in the External Core file because it's not
+-- straightforward to derive its definition from the newtype declaration alone.
+-- At the same time, we need the newtype decl to declare the tycon itself.
+-- Sigh.
+  text "%newtype" <+> pqname tcon <+> (hsep (map ptbind tbinds)) 
+    <+> axiomclause <+> repclause
+       where  axiomclause = char '^' <+> parens (pqname coercion <+> text "::"
+                                     <+> pkind k)
+              repclause   = case rep of
+                              Just ty -> char '=' <+> pty ty 
+                             Nothing -> empty
+             
 
 pcdef :: Cdef -> Doc
 pcdef (Constr dcon tbinds tys)  =
@@ -84,7 +95,8 @@ pakind (Kopen) = char '?'
 pakind k = parens (pkind k)
 
 pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
-pkind (Keq t1 t2) = parens (pty t1 <> text ":=:" <> pty t2)
+pkind (Keq t1 t2) = parens (parens (pty t1) <+> text ":=:" <+> 
+                            parens (pty t2))
 pkind k = pakind k
 
 paty, pbty, pty :: Ty -> Doc
@@ -113,13 +125,12 @@ pvdefg (Rec vdefs) = text "%rec" $$ braces (indent (vcat (punctuate (char ';') (
 pvdefg (Nonrec vdef) = pvdef vdef
 
 pvdef :: Vdef -> Doc
-pvdef (l,v,t,e) = sep [plocal l <+> pname v <+> text "::" <+> pty t <+> char '=',
+-- note: at one point every vdef was getting printed out as "local".
+-- I think that's manifestly wrong. Right now, the "%local" keyword
+-- is never used.
+pvdef (_l,v,t,e) = sep [pname v <+> text "::" <+> pty t <+> char '=',
                    indent (pexp e)]
 
-plocal :: Bool -> Doc
-plocal True  = text "%local"
-plocal False = empty
-
 paexp, pfexp, pexp :: Exp -> Doc
 paexp (Var x) = pqname x
 paexp (Dcon x) = pqname x

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index ddcb665..e6366be 100644 (file)
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -186,7 +186,7 @@ data TyCon
         tyConName   :: Name,
        tyConArity  :: Arity,
        coKindFun   :: [Type] -> (Type,Type)
-    }          -- INVARAINT: coKindFun is always applied to exactly 'arity' args
+    }          -- INVARIANT: coKindFun is always applied to exactly 'arity' args
                -- E.g. for trans (c1 :: ta=tb) (c2 :: tb=tc), the coKindFun returns 
                --      the kind as a pair of types: (ta,tc)
        
@@ -372,7 +372,7 @@ Source code:
        w2 :: Foo T
        w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
 
-After desugaring, and discading the data constructors for the newtypes,
+After desugaring, and discarding the data constructors for the newtypes,
 we get:
        w2 :: Foo T
        w2 = w1