Improve External Core syntax for newtypes

I was confused by the newtype eta-contraction trick before.
Newtype declarations are much less redundant now.

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

diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs
index ba0c198..99ea425 100644 (file)
--- a/compiler/coreSyn/MkExternalCore.lhs
+++ b/compiler/coreSyn/MkExternalCore.lhs
@@ -84,14 +84,12 @@ collect_tdefs tcon tdefs
   | isAlgTyCon tcon = tdef: tdefs
   where
     tdef | isNewTyCon tcon = 
-                C.Newtype (qtc tcon) (map make_tbind tyvars) 
+                C.Newtype (qtc tcon) 
                   (case newTyConCo_maybe tcon of
-                     Just co -> (qtc co, 
-                        map make_tbind vs, 
-                        make_kind (mkCoKind l r))
-                       where (vs,l,r) = coercionAxiom co
+                     Just co -> qtc co
                      Nothing       -> pprPanic ("MkExternalCore: newtype tcon\
                                        should have a coercion: ") (ppr tcon))
+                  (map make_tbind tyvars) 
                    repclause 
          | otherwise = 
                 C.Data (qtc tcon) (map make_tbind tyvars) 
@@ -99,18 +97,6 @@ collect_tdefs tcon tdefs
          where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing
                         | otherwise = Just (make_ty (snd (newTyConRhs tcon)))
     tyvars = tyConTyVars tcon
-    coercionAxiom co = 
-      case isCoercionTyCon_maybe co of
-        -- See Note [Newtype coercions] in 
-        -- types/TyCon
-        Just (arity,coKindFun) | (l,r) <- (coKindFun $ map mkTyVarTy vs) -> 
-             -- Here we eta-expand the newtype coercion,
-             -- which makes the ext-core typechecker somewhat simpler.
-            (tyvars,mkAppTys l extraVs,mkAppTys r extraVs)
-               where (vs, extraVs) = (take arity tyvars,
-                        map mkTyVarTy $ drop arity tyvars)
-        Nothing -> pprPanic "MkExternalCore: coercion tcon lacks a kind fun"
-                     (ppr tcon)
 
 collect_tdefs _ tdefs = tdefs
 

diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs
index fb4fc45..c34f7b8 100644 (file)
--- a/compiler/coreSyn/PprExternalCore.lhs
+++ b/compiler/coreSyn/PprExternalCore.lhs
@@ -54,22 +54,12 @@ 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 (coercion,tbs,k) rep) =
--- TODO: I think this is kind of redundant now.
--- 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)) 
-    $$ indent (axiomclause $$ repclause)
-       where  axiomclause = char '^' 
-                 <+> parens (pqname coercion <+> (hsep (map ptbind tbs))
-                              <+> text "::"
-                              <+> pkind k)
-              repclause   = case rep of
-                              Just ty -> char '=' <+> pty ty 
-                             Nothing -> empty
+ptdef (Newtype tcon coercion tbinds rep) =
+  text "%newtype" <+> pqname tcon <+> pqname coercion 
+   <+> (hsep (map ptbind tbinds)) $$ indent repclause
+       where repclause = case rep of
+                           Just ty -> char '=' <+> pty ty 
+                          Nothing -> empty
              
 
 pcdef :: Cdef -> Doc

diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
index cab3e62..af3bb3c 100644 (file)
--- a/utils/ext-core/Check.hs
+++ b/utils/ext-core/Check.hs
@@ -124,13 +124,12 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef
               tcenv' <- extendM NotTv tcenv (c, Kind k)
               return (tcenv',tsenv)
            where k = foldr Karrow Klifted (map snd tbs)
-       ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = 
+       ch (Newtype (m,c) coVar tbs rhs) = 
            do mn <- getMname
                requireModulesEq m mn "newtype declaration" tdef False
               tcenv' <- extendM NotTv tcenv (c, Kind k)
                -- add newtype axiom to env
-               tcenv'' <- extendM NotTv tcenv' 
-                  (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
+               tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
               tsenv' <- case rhs of
                           Nothing -> return tsenv
                           Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
@@ -142,15 +141,30 @@ processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
       where 
        ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
            where k = foldr Karrow Klifted (map snd tbs)
-       ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = 
+       ch (Newtype tc@(_,c) coercion tbs rhs) = 
            let tcenv' = eextend tcenv (c, Kind k)
                 -- add newtype axiom to env
-                tcenv'' = eextend tcenv' 
-                  (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
+                tcenv'' = case rhs of
+                            Just rep ->
+                              eextend tcenv' 
+                               (snd coercion, Coercion $ DefinedCoercion tbs
+                                (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep))
+                            Nothing -> tcenv'
                tsenv' = maybe tsenv 
                   (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
                (tcenv'', tsenv')
            where k = foldr Karrow Klifted (map snd tbs)
+
+envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Maybe Ty 
+  -> CheckResult Tcenv
+envPlusNewtype tcenv tyCon coVar tbs rhs =
+  case rhs of
+    Nothing -> return tcenv
+    Just rep -> extendM NotTv tcenv 
+                  (snd coVar, Coercion $ DefinedCoercion tbs
+                            (foldl Tapp (Tcon tyCon) 
+                                       (map Tvar (fst (unzip tbs))),
+                                       rep))
     
 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
 checkTdef tcenv cenv = ch
@@ -173,17 +187,12 @@ checkTdef tcenv cenv = ch
                                  (foldr tArrow
                                          (foldl Tapp (Tcon (Just mn,c))
                                                 (map (Tvar . fst) utbs)) ts) tbs
-         ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) =  
+         ch (tdef@(Newtype tc _ tbs (Just t))) =  
            do tvenv <- foldM (extendM Tv) eempty tbs
-              k <- checkTy (tcenv,tvenv) t
-               -- Makes sure GHC is eta-expanding things properly
-               require (length tbs == length coTbs) $
-                 ("Arity mismatch between newtycon and newtype coercion: "
-                  ++ show tdef)
-               require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
-               axiomTvenv <- foldM (extendM Tv) eempty coTbs
-               kLhs <- checkTy (tcenv,axiomTvenv) coLhs
-               kRhs <- checkTy (tcenv,axiomTvenv) coRhs
+              kRhs <- checkTy (tcenv,tvenv) t
+               require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
+               kLhs <- checkTy (tcenv,tvenv) 
+                         (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
                require (kLhs `eqKind` kRhs) 
                   ("Kind mismatch in newtype axiom types: " ++ show tdef 
                     ++ " kinds: " ++

diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs
index 66270cd..0fb48b8 100644 (file)
--- a/utils/ext-core/Core.hs
+++ b/utils/ext-core/Core.hs
@@ -9,14 +9,15 @@ data Module
 
 data Tdef 
   = Data (Qual Tcon) [Tbind] [Cdef]
-  | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty)
+    -- type constructor; coercion name; type arguments; type rep
+    -- If we have: (Newtype tc co tbs (Just t))
+    -- there is an implicit axiom:
+    --  co tbs :: tc tbs :=: t
+  | Newtype (Qual Tcon) (Qual Tcon) [Tbind] (Maybe Ty)
 
 data Cdef 
   = Constr (Qual Dcon) [Tbind] [Ty]
 
--- Newtype coercion
-type Axiom = (Qual Tcon, [Tbind], (Ty,Ty))
-
 data Vdefg 
   = Rec [Vdef]
   | Nonrec Vdef

diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs
index 42e21e9..4afa924 100644 (file)
--- a/utils/ext-core/ParsecParser.hs
+++ b/utils/ext-core/ParsecParser.hs
@@ -36,7 +36,6 @@ coreModuleName = do
 
 corePackageName :: Parser Pname
 -- Package names can be lowercase or uppercase!
--- TODO: update docs
 corePackageName = identifier <|> upperName
 
 coreHierModuleNames :: Parser ([Id], Id)
@@ -81,11 +80,11 @@ coreNewtypeDecl = do
   reserved "newtype"
   tyCon  <- coreQualifiedCon
   whiteSpace
+  coercionName <- coreQualifiedCon
+  whiteSpace
   tBinds <- coreTbinds
-  symbol "^"
-  axiom <- coreAxiom
   tyRep  <- try coreTRep
-  return $ Newtype tyCon tBinds axiom tyRep
+  return $ Newtype tyCon coercionName tBinds tyRep
 
 coreQualifiedCon :: Parser (Mname, Id)
 coreQualifiedCon = coreQualifiedGen upperName
@@ -109,17 +108,6 @@ coreQualifiedGen p = (try (do
    -- unqualified name
    (p >>= (\ res -> return (Nothing, res)))
 
-coreAxiom :: Parser Axiom
-coreAxiom = parens (do
-              coercionName <- coreQualifiedCon
-              whiteSpace
-              tbs <- coreTbinds
-              whiteSpace
-              symbol "::"
-              whiteSpace
-              coercionK <- try equalityKind <|> parens equalityKind
-              return (coercionName, tbs, coercionK))
-
 coreTbinds :: Parser [Tbind]
 coreTbinds = many coreTbind 
 
@@ -322,7 +310,7 @@ coreVdef = do
 coreAtomicExp :: Parser Exp
 coreAtomicExp = do
 -- For stupid reasons, the whiteSpace is necessary.
--- Without it, (pt coreAppExp "w ^a:B.C ") doesn't work.
+-- Without it, (pt coreAppExp "w a:B.C ") doesn't work.
   whiteSpace
   res <- choice [try coreDconOrVar,
                     try coreLit,

diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs
index 2649a00..4e42445 100644 (file)
--- a/utils/ext-core/Printer.hs
+++ b/utils/ext-core/Printer.hs
@@ -66,14 +66,10 @@ ptdef (Data qtcon tbinds cdefs) =
   (text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=')
   $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
 
-ptdef (Newtype qtcon tbinds (coercion,cTbs,k) tyopt) =
-  text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds))
-    $$ indent (axiomclause $$ repclause)
-       where axiomclause = char '^' <+> parens (pqname coercion <+> 
-                                          (hsep (map ptbind cTbs)) <+>
-                                          text "::"
-                                      <+> peqkind k)
-            repclause = case tyopt of
+ptdef (Newtype qtcon coercion tbinds tyopt) =
+  text "%newtype" <+> pqname qtcon <+> pqname coercion 
+    <+> (hsep (map ptbind tbinds)) $$ indent repclause
+       where repclause = case tyopt of
                            Just ty -> char '=' <+> pty ty 
                            Nothing -> empty