- deriving (Eq)
-
-data Lit
- = Lint Integer Ty
- | Lrational Rational Ty
- | Lchar Char Ty
- | Lstring String Ty
- deriving (Eq) -- with nearlyEqualTy
-
--- new: Pnames
--- this requires at least one module name,
--- and possibly other hierarchical names
--- an alternative would be to flatten the
+ | Keq Ty Ty
+
+-- A CoercionKind isn't really a Kind at all, but rather,
+-- corresponds to an arbitrary user-declared axiom.
+-- A tycon whose CoercionKind is (DefinedCoercion <tbs> (from, to))
+-- represents a tycon with arity (length tbs), whose kind is
+-- (from :=: to) (modulo substituting type arguments.
+-- It's not a Kind because a coercion must always be fully applied:
+-- whenever we see a tycon that has such a CoercionKind, it must
+-- be fully applied if it's to be assigned an actual Kind.
+-- So, a CoercionKind *only* appears in the environment (mapping
+-- newtype axioms onto CoercionKinds).
+-- Was that clear??
+data CoercionKind =
+ DefinedCoercion [Tbind] (Ty,Ty)
+
+-- The type constructor environment maps names that are
+-- either type constructors or coercion names onto either
+-- kinds or coercion kinds.
+data KindOrCoercion = Kind Kind | Coercion CoercionKind
+
+data Lit = Literal CoreLit Ty
+ deriving Eq -- with nearlyEqualTy
+
+data CoreLit = Lint Integer
+ | Lrational Rational
+ | Lchar Char
+ | Lstring String
+ deriving Eq
+
+-- Right now we represent module names as triples:
+-- (package name, hierarchical names, leaf name)
+-- An alternative to this would be to flatten the