ref: 9450806259eb31116552c4b1b173ee68071d0b6d
parent: 65a2249a1ba81f0448c0e9f02e9d65d176b88cfd
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Mon Dec 16 12:44:10 EST 2024
Type equality (~) should be polykinded. Fixes issue #71
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -555,14 +555,6 @@
kTypeTypeTypeS :: EType
kTypeTypeTypeS = kArrow kType $ kArrow kType kType
--- (=>) :: Constraint -> Type -> Type
---kConstraintTypeTypeS :: EType
---kConstraintTypeTypeS = kArrow kConstraint $ kArrow kType kType
-
--- (~) :: Type -> Type -> Constraint
-kTypeTypeConstraintS :: EType
-kTypeTypeConstraintS = kArrow kType (kArrow kType kConstraint)
-
mkIdentB :: String -> Ident
mkIdentB = mkIdentSLoc builtinLoc
@@ -610,11 +602,16 @@
kv = EVar k
kk = IdKind k sKind
-- Tuples are polykinded since they need to handle both Type and Constraint
+ -- (,) :: forall k . k -> k -> k
+ -- etc.
tuple n =
let
i = tupleConstr builtinLoc n
in (i, [entry i $ EForall True [kk] $ foldr kArrow kv (replicate n kv)])
+ -- (=>) :: forall k . Constraint -> k -> k
kImplies = EForall True [kk] $ kConstraint `kArrow` (kv `kArrow` kv)
+ -- (~) :: forall k . k -> k -> Constraint
+ kTypeEqual = EForall True [kk] $ kv `kArrow` (kv `kArrow` kConstraint)
in
[
-- The function arrow et al are bothersome to define in Primitives, so keep them here.
@@ -621,7 +618,7 @@
-- But the fixity is defined in Primitives.
(mkIdentB "->", [entry identArrow kTypeTypeTypeS]),
(mkIdentB "=>", [entry identImplies kImplies]),
- (mkIdentB "~", [entry identTypeEq kTypeTypeConstraintS]),
+ (mkIdentB "~", [entry identTypeEq kTypeEqual]),
-- Primitives.hs uses the type [], and it's annoying to fix that.
-- XXX should not be needed
(identList, [entry identList kTypeTypeS]),