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.
Invariant: The list of alternatives is ALWAYS EXHAUSTIVE,
meaning that it covers all cases that can occur
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
data Foo = Red | Green | Blue
...case x of
data Tdef
= Data (Qual Tcon) [Tbind] [Cdef]
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
data Cdef
= Constr Dcon [Tbind] [Ty]
| GadtConstr Dcon Ty
+-- Newtype coercion
+type Axiom = (Qual Tcon, Kind)
+
data Vdefg
= Rec [Vdef]
| Nonrec Vdef
data Vdefg
= Rec [Vdef]
| Nonrec Vdef
| isAlgTyCon tcon = tdef: tdefs
where
tdef | isNewTyCon tcon =
| 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
- 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
where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing
| otherwise = Just (make_ty (repType rhs))
where (_, rhs) = newTyConRhs tcon
collect_tdefs _ tdefs = 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
make_cdef :: DataCon -> C.Cdef
make_cdef dcon = C.Constr dcon_name existentials tys
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 (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
(map make_ty ts)
-- Newtypes are treated just like any other type constructor; not expanded
-- Reason: predTypeRep does substitution and, while substitution deals
\begin{code}
module PprExternalCore () where
\begin{code}
module PprExternalCore () where
+import Pretty
+import Char
+
+
instance Show Module where
showsPrec _ m = shows (pmodule m)
instance Show Module where
showsPrec _ m = shows (pmodule m)
(text "%data" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> char '=')
$$ indent (braces ((vcat (punctuate (char ';') (map pcdef 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) =
pcdef :: Cdef -> Doc
pcdef (Constr dcon tbinds tys) =
pakind k = parens (pkind k)
pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
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
pkind k = pakind k
paty, pbty, pty :: Ty -> Doc
pvdefg (Nonrec vdef) = pvdef vdef
pvdef :: Vdef -> Doc
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 '=',
-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
paexp, pfexp, pexp :: Exp -> Doc
paexp (Var x) = pqname x
paexp (Dcon x) = pqname x
tyConName :: Name,
tyConArity :: Arity,
coKindFun :: [Type] -> (Type,Type)
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)
-- E.g. for trans (c1 :: ta=tb) (c2 :: tb=tc), the coKindFun returns
-- the kind as a pair of types: (ta,tc)
w2 :: Foo T
w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
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
we get:
w2 :: Foo T
w2 = w1