ref: 39d5ddcff88302a615865b5c9a58b9a82d71bd35
parent: 576b6afdd977043d4d1c5d04d569b64d11829c54
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Fri Oct 13 20:38:14 EDT 2023
Add kind checking for class and instance
--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
v4.0
980
-((A :0 _863) ((A :1 ((B _910) _0)) ((A :2 (((S' _910) _0) I)) ((A :3 _833) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _862) ((C _74) _5))) ((A :7 (((C' _6) (_881 _71)) ((_74 _879) _70))) ((A :8 ((B ((S _910) _879)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_74 _189)) _10)) ((A :12 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_73 _9)) P)) ((A :15 ((B (B (_73 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 ((B (_73 _9)) (B (P _791)))) ((A :18 ((B (_73 _9)) (BK (P _791)))) ((A :19 ((_73 _9) ((S P) I))) ((A :20 ((B (_73 _9)) ((C (S' P)) I))) ((A :21 ((B Y) ((B (B (P (_14 _114)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _115)))))) ((A :22 ((B Y) ((B (B (P (_14 _791)))) ((B (C' B)) (B _13))))) ((A :23 _3) ((A :24 (T (_14 _791))) ((A :25 (_21 _75)) ((A :26 (R _33)) ((A :27 (T _32)) ((A :28 ((P _33) _32)) ((A :29 _33) ((A :30 ((C ((C S') _28)) I)) ((A :31 ((C S) _28)) ((A :32 K) ((A :33 A) ((A :34 _838) ((A :35 _839) ((A :36 (((S' _27) (_830 #97)) ((C _830) #122))) ((A :37 (((S' _27) (_830 #65)) ((C _830) #90))) ((A :38 (((S' _26) _36) _37)) ((A :39 (((S' _27) (_830 #48)) ((C _830) #57))) ((A :40 (((S' _27) (_830 #32)) ((C _830) #126))) ((A :41 _827) ((A :42 _828) ((A :43 _830) ((A :44 _829) ((A :45 (((S' _26) ((C _41) #32)) (((S' _26) ((C _41) #9)) ((C _41) #10)))) ((A :46 ((S ((S (((S' _27) (_43 #65)) ((C _43) #90))) (_33 (((_790 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #65))) (_35 #97))))) ((A :47 ((S ((S (((S' _27) (_43 #97)) ((C _43) #97))) (_33 (((_790 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #97))) (_35 #65))))) ((A :48 _798) ((A :49 _799) ((A :50 _800) ((A :51 _801) ((A :52 (_49 %0.0)) ((A :53 _48) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _802) ((A :58 _803) ((A :59 _57) ((A :60 _58) ((A :61 _804) ((A :62 _805) ((A :63 _806) ((A :64 _807) ((A :65 _61) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _808) ((A :70 ((B BK) T)) ((A :71 (BK T)) ((A :72 P) ((A :73 I) ((A :74 B) ((A :75 I) ((A :76 K) ((A :77 C) ((A :78 _834) ((A :79 ((C ((C S') _189)) _190)) ((A :80 (((C' (S' (C' B))) B) I)) ((A :81 _792) ((A :82 _793) ((A :83 _794) ((A :84 _795) ((A :85 _796) ((A :86 _797) ((A :87 (_82 #0)) ((A :88 _815) ((A :89 _816) ((A :90 _817) ((A :91 _818) ((A :92 _819) ((A :93 _820) ((A :94 _88) ((A :95 (BK K)) ((A :96 ((B BK) ((B (B BK)) P))) ((A :97 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :98 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _26) (_91 #0))) (_88 #0)))) ((B (B ((C' P) (_86 #1)))) _81))) (C P))) _84)) _85)) ((A :99 _95) ((A :100 (((S' C) ((B (P _177)) (((C' (C' B)) (((C' C) _88) _177)) _178))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_88 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_88 #1)))) ((B ((C' C) ((B ((C' S') (_88 #2))) (C _100)))) (C _100))))) (C _100))))) (C _100)))) (T K))) (T A)))) ((C _98) #4)))) ((A :101 (_107 _76)) ((A :102 ((_122 (_79 _101)) _99)) ((A :103 ((C (((C' B) ((P _114) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _104)))) (((S' (C' (C' B))) ((B (B (B _104))) (((S' (C' B)) ((B (B _104)) (((C' B) ((B _120) (T #0))) _103))) (((C' B) ((B _120) (T #1))) _103)))) (((C' B) ((B _120) (T #2))) _103)))) (((C' B) ((B _120) (T #3))) _103)))) ((B T) ((B (B P)) ((C' _81) (_83 #4)))))) ((A :104 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _90)))) ((B ((C' B) _115)) _104)))))) ((B ((C' B) _115)) (C _104)))))))))) (((_790 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :105 ((_74 (_120 _189)) _103)) ((A :106 (((C' C) (((C' C) (C _100)) (_3 "Data.IntMap.!"))) I)) ((A :107 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B ((S' B) ((B (S' P)) (C _96)))) ((B (B ((C' (S' C
\ No newline at end of file
+((A :0 _864) ((A :1 ((B _910) _0)) ((A :2 (((S' _910) _0) I)) ((A :3 _834) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _863) ((C _74) _5))) ((A :7 (((C' _6) (_881 _71)) ((_74 _879) _70))) ((A :8 ((B ((S _910) _879)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_74 _189)) _10)) ((A :12 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_73 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_73 _9)) P)) ((A :15 ((B (B (_73 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 ((B (_73 _9)) (B (P _792)))) ((A :18 ((B (_73 _9)) (BK (P _792)))) ((A :19 ((_73 _9) ((S P) I))) ((A :20 ((B (_73 _9)) ((C (S' P)) I))) ((A :21 ((B Y) ((B (B (P (_14 _114)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _115)))))) ((A :22 ((B Y) ((B (B (P (_14 _792)))) ((B (C' B)) (B _13))))) ((A :23 _3) ((A :24 (T (_14 _792))) ((A :25 (_21 _75)) ((A :26 (R _33)) ((A :27 (T _32)) ((A :28 ((P _33) _32)) ((A :29 _33) ((A :30 ((C ((C S') _28)) I)) ((A :31 ((C S) _28)) ((A :32 K) ((A :33 A) ((A :34 _839) ((A :35 _840) ((A :36 (((S' _27) (_831 #97)) ((C _831) #122))) ((A :37 (((S' _27) (_831 #65)) ((C _831) #90))) ((A :38 (((S' _26) _36) _37)) ((A :39 (((S' _27) (_831 #48)) ((C _831) #57))) ((A :40 (((S' _27) (_831 #32)) ((C _831) #126))) ((A :41 _828) ((A :42 _829) ((A :43 _831) ((A :44 _830) ((A :45 (((S' _26) ((C _41) #32)) (((S' _26) ((C _41) #9)) ((C _41) #10)))) ((A :46 ((S ((S (((S' _27) (_43 #65)) ((C _43) #90))) (_33 (((_791 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #65))) (_35 #97))))) ((A :47 ((S ((S (((S' _27) (_43 #97)) ((C _43) #97))) (_33 (((_791 "lib/Data/Char.hs") #3) #8)))) ((B _34) (((C' _81) (((C' _82) _35) (_35 #97))) (_35 #65))))) ((A :48 _799) ((A :49 _800) ((A :50 _801) ((A :51 _802) ((A :52 (_49 %0.0)) ((A :53 _48) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _803) ((A :58 _804) ((A :59 _57) ((A :60 _58) ((A :61 _805) ((A :62 _806) ((A :63 _807) ((A :64 _808) ((A :65 _61) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _809) ((A :70 ((B BK) T)) ((A :71 (BK T)) ((A :72 P) ((A :73 I) ((A :74 B) ((A :75 I) ((A :76 K) ((A :77 C) ((A :78 _835) ((A :79 ((C ((C S') _189)) _190)) ((A :80 (((C' (S' (C' B))) B) I)) ((A :81 _793) ((A :82 _794) ((A :83 _795) ((A :84 _796) ((A :85 _797) ((A :86 _798) ((A :87 (_82 #0)) ((A :88 _816) ((A :89 _817) ((A :90 _818) ((A :91 _819) ((A :92 _820) ((A :93 _821) ((A :94 _88) ((A :95 (BK K)) ((A :96 ((B BK) ((B (B BK)) P))) ((A :97 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :98 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _26) (_91 #0))) (_88 #0)))) ((B (B ((C' P) (_86 #1)))) _81))) (C P))) _84)) _85)) ((A :99 _95) ((A :100 (((S' C) ((B (P _177)) (((C' (C' B)) (((C' C) _88) _177)) _178))) ((B ((C' (C' (C' C))) (((C' (C' (C' C))) (((C' (C' (C' (C' S')))) ((B (B (B (B C)))) ((B ((C' (C' (C' C))) ((B (B (B ((S' S') (_88 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_88 #1)))) ((B ((C' C) ((B ((C' S') (_88 #2))) (C _100)))) (C _100))))) (C _100))))) (C _100)))) (T K))) (T A)))) ((C _98) #4)))) ((A :101 (_107 _76)) ((A :102 ((_122 (_79 _101)) _99)) ((A :103 ((C (((C' B) ((P _114) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _104)))) (((S' (C' (C' B))) ((B (B (B _104))) (((S' (C' B)) ((B (B _104)) (((C' B) ((B _120) (T #0))) _103))) (((C' B) ((B _120) (T #1))) _103)))) (((C' B) ((B _120) (T #2))) _103)))) (((C' B) ((B _120) (T #3))) _103)))) ((B T) ((B (B P)) ((C' _81) (_83 #4)))))) ((A :104 ((S S) ((B BK) ((B BK) (((S' S) T) ((B BK) ((B BK) ((C (((S' C') S) ((B (B (B (S B)))) ((B (B (B (B (B BK))))) ((B ((S' (C' B)) ((B B') B'))) ((B (B (B (B (B (S B)))))) ((B (B (B (B (B (B (B BK))))))) (((C' B) (B' (B' ((B (C' (C' (C' C)))) ((B ((C' B) (B' ((B C) _90)))) ((B ((C' B) _115)) _104)))))) ((B ((C' B) _115)) (C _104)))))))))) (((_791 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :105 ((_74 (_120 _189)) _103)) ((A :106 (((C' C) (((C' C) (C _100)) (_3 "Data.IntMap.!"))) I)) ((A :107 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B ((S' B) ((B (S' P)) (C _96)))) ((B (B ((C' (S' C
\ No newline at end of file
--- a/src/MicroHs/Desugar.hs
+++ b/src/MicroHs/Desugar.hs
@@ -49,7 +49,7 @@
ForImp ie i _ -> [(i, Lit $ LForImp ie)]
Infix _ _ -> []
Class _ _ _ -> [] -- XXX probably needs a default instance
- Instance _ _ _ -> [] -- XXX probably needs instance record
+ Instance _ _ _ _ -> [] -- XXX probably needs instance record
oneAlt :: Expr -> EAlts
oneAlt e = EAlts [([], e)] []
--- a/src/MicroHs/Expr.hs
+++ b/src/MicroHs/Expr.hs
@@ -63,8 +63,8 @@
| Import ImportSpec
| ForImp String Ident EType
| Infix Fixity [Ident]
- | Class (Maybe EConstraint) LHS [EBind]
- | Instance (Maybe EConstraint) EType [EBind] -- no deriving yet
+ | Class (Maybe EConstraint) LHS [EBind] -- XXX will probable need initial forall with FD
+ | Instance [IdKind] (Maybe EConstraint) EConstraint [EBind] -- no deriving yet
--Xderiving (Show, Eq)
data ImportSpec = ImportSpec Bool Ident (Maybe Ident) (Maybe (Bool, [ImportItem])) -- first Bool indicates 'qualified', second 'hiding'
@@ -380,7 +380,7 @@
Infix (a, p) is -> "infix" ++ f a ++ " " ++ showInt p ++ " " ++ intercalate ", " (map showIdent is)
where f AssocLeft = "l"; f AssocRight = "r"; f AssocNone = ""
Class sup lhs bs -> "class " ++ ctx sup ++ showLHS lhs ++ showWhere bs
- Instance ct ty bs -> "instance " ++ ctx ct ++ showEType ty ++ showWhere bs
+ Instance vs ct ty bs -> "instance " ++ showForall vs ++ ctx ct ++ showEType ty ++ showWhere bs
where ctx Nothing = ""
ctx (Just t) = showEType t ++ " => "
@@ -403,7 +403,7 @@
showWhere :: [EBind] -> String
showWhere [] = ""
-showWhere bs = "where\n" ++ unlines (map showEBind bs)
+showWhere bs = " where\n" ++ unlines (map showEBind bs)
showAltsL :: String -> [EAlt] -> String
showAltsL sep [([], e)] = " " ++ sep ++ " " ++ showExpr e
@@ -433,14 +433,19 @@
EAt i e -> showIdent i ++ "@" ++ showExpr e
EUVar i -> "a" ++ showInt i
ECon c -> showCon c
- EForall iks e -> "forall " ++ unwords (map showIdKind iks) ++ " . " ++ showEType e
+ EForall iks e -> showForall iks ++ showEType e
where
showApp as (EApp f a) = showApp (a:as) f
showApp as (EVar i) | eqString op "->", [a, b] <- as = "(" ++ showExpr a ++ " -> " ++ showExpr b ++ ")"+ | eqString op "=>", [a, b] <- as = showExpr a ++ " => " ++ showExpr b
| eqChar (head op) ',' = showExpr (ETuple as)
| eqString op "[]", length as == 1 = showExpr (EListish (LList as))
where op = unQualString (unIdent i)
showApp as f = "(" ++ unwords (map showExpr (f:as)) ++ ")"+
+showForall :: [IdKind] -> String
+showForall [] = ""
+showForall iks = "forall " ++ unwords (map showIdKind iks) ++ " . "
showListish :: Listish -> String
showListish _ = "<<Listish>>"
--- a/src/MicroHs/Parse.hs
+++ b/src/MicroHs/Parse.hs
@@ -258,7 +258,7 @@
<|< ForImp <$> (pKeyword "foreign" *> pKeyword "import" *> pKeyword "ccall" *> pString) <*> pLIdent <*> (pSymbol "::" *> pType)
<|< Infix <$> ((,) <$> pAssoc <*> pPrec) <*> esepBy1 pTypeOper (pSpec ',')
<|< Class <$> (pKeyword "class" *> pContext) <*> pLHS <*> pWhere pClsBind
- <|< Instance <$> (pKeyword "instance" *> pContext) <*> pTypeApp <*> pWhere pClsBind
+ <|< Instance <$> (pKeyword "instance" *> pForall) <*> pContext <*> pTypeApp <*> pWhere pClsBind
where
pAssoc = (AssocLeft <$ pKeyword "infixl") <|< (AssocRight <$ pKeyword "infixr") <|< (AssocNone <$ pKeyword "infix")
dig (TInt _ i) | -2 <= i && i <= 9 = Just i
@@ -299,9 +299,12 @@
-- in lambda and 'case'.
pType :: P EType
pType = P.do
- vs <- (pKeyword "forall" *> esome pIdKind <* pSymbol ".") <|< pure []
+ vs <- pForall
t <- pTypeOp
pure $ if null vs then t else EForall vs t
+
+pForall :: P [IdKind]
+pForall = (pKeyword "forall" *> esome pIdKind <* pSymbol ".") <|< pure []
pTypeOp :: P EType
pTypeOp = pOperators pTypeOper pTypeArg
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -348,11 +348,12 @@
entry i = Entry (EVar (mkIdentB i))
in M.fromList [
-- The kinds are wired in (for now)
- (mkIdentB "Primitives.Type", [entry "Primitives.Type" kTypeS]),
- (mkIdentB "Type", [entry "Primitives.Type" kTypeS]),
- (mkIdentB "Constraint", [entry "Primitives.Constraint" kTypeS]),
- (mkIdentB "Primitives.->", [entry "Primitives.->" kTypeTypeTypeS]),
- (mkIdentB "->", [entry "Primitives.->" kTypeTypeTypeS])
+ (mkIdentB "Primitives.Type", [entry "Primitives.Type" kTypeS]),
+ (mkIdentB "Type", [entry "Primitives.Type" kTypeS]),
+ (mkIdentB "Constraint", [entry "Primitives.Constraint" kTypeS]),
+ (mkIdentB "Primitives.Constraint", [entry "Primitives.Constraint" kTypeS]),
+ (mkIdentB "Primitives.->", [entry "Primitives.->" kTypeTypeTypeS]),
+ (mkIdentB "->", [entry "Primitives.->" kTypeTypeTypeS])
]
primTypes :: [(Ident, [Entry])]
@@ -531,53 +532,6 @@
else
setUVar r1 t2
-{--unify :: --XHasCallStack =>
- SLoc -> EType -> EType -> T ()
-unify loc a b = T.do
--- traceM ("unify1 " ++ showExpr a ++ " = " ++ showExpr b)- aa <- expandType a
- bb <- expandType b
--- traceM ("unify2 " ++ showExpr aa ++ " = " ++ showExpr bb)- unifyR loc aa bb
-
--- XXX should do occur check
-unifyR :: --XHasCallStack =>
- SLoc -> EType -> EType -> T ()
-unifyR loc a b = T.do
- let
- bad = tcError loc $ "Cannot unify " ++ showExpr a ++ " and " ++ showExpr b ++ "\n"
- case a of
- EVar ia ->
- case b of
- EVar ib -> if eqIdent ia ib then T.return () else bad
- EApp _ _ -> bad
- EUVar i -> addUVar i a
- _ -> impossible
- EApp fa xa ->
- case b of
- EVar _ -> bad
- EApp fb xb -> T.do { unify loc fa fb; unify loc xa xb }- EUVar i -> addUVar i a
- _ ->
- --Xtrace ("impossible unify 1 " ++ showExpr a ++ " = " ++ showExpr b) $- impossible
- EUVar i -> addUVar i b
- _ -> --Xtrace ("impossible unify 2 " ++ showExpr a ++ " = " ++ showExpr b) $- impossible
--}
-
-{--unMType :: Expected -> T EType
-unMType mt =
- case mt of
- Infer r -> T.do
- t <- newUVar
- tSetRefType r t
- T.return t
- Check t -> T.return t
--}
-
-- Reset type variable and unification map
tcReset :: T ()
tcReset = T.do
@@ -710,6 +664,7 @@
T.mapM_ addTypeKind dsk -- Add the kind of each type to the environment
T.mapM tcDefType dsk
+-- Make sure that the kind expressions are well formed.
tcDefKind :: EDef -> T EDef
tcDefKind adef = T.do
tcReset
@@ -720,6 +675,8 @@
case at of
ESign t k -> withVks vks k $ \ vvks kr -> T.return $ Type (i, vvks) (ESign t kr)
_ -> withVks vks kType $ \ vvks _ -> T.return $ Type (i, vvks) at
+ Class ctx (i, vks) ms-> withVks vks kConstraint $ \ vvks _ -> T.return $ Class ctx (i, vvks) ms
+ Instance vks ctx t d -> withVks vks kConstraint $ \ vvks _ -> T.return $ Instance vvks ctx t d
_ -> T.return adef
-- Check&rename the given kinds, apply reconstruction at the end
@@ -737,6 +694,7 @@
loop [] vks
fun nvks nkr
+-- Add symbol table entries (with kind) for all top level typeish definitions
addTypeKind :: EDef -> T ()
addTypeKind adef = T.do
tcReset
@@ -744,6 +702,7 @@
Data lhs _ -> addLHSKind lhs kType
Newtype lhs _ _ -> addLHSKind lhs kType
Type lhs t -> addLHSKind lhs (getTypeKind t)
+ Class _ lhs _ -> addLHSKind lhs kConstraint
_ -> T.return ()
getTypeKind :: EType -> EKind
@@ -768,6 +727,8 @@
extSyn (qualIdent mn i) (EForall vs t)
_ -> T.return ()
+-- Do kind checking of all typeish definitions.
+-- XXX check method signatures?
tcDefType :: EDef -> T EDef
tcDefType d = T.do
tcReset
@@ -777,7 +738,14 @@
Type lhs t -> Type lhs <$> withVars (snd lhs) (tcInferTypeT t)
Sign i t -> (Sign i ) <$> tcTypeT (Check kType) t
ForImp ie i t -> (ForImp ie i) <$> tcTypeT (Check kType) t
- _ -> T.return d
+ Class mc lhs m -> withVars (snd lhs) $ Class <$> tcCtx mc <*> pure lhs <*> mapM tcMethod m
+ Instance vs mc t m -> withVars vs $ Instance vs <$> tcCtx mc <*> tcTypeT (Check kConstraint) t <*> pure m
+ _ -> T.return d
+ where
+ tcCtx Nothing = pure Nothing
+ tcCtx (Just c) = Just <$> tcTypeT (Check kConstraint) c
+ tcMethod (BSign i t) = BSign i <$> tcTypeT (Check kType) t
+ tcMethod m = pure m
withVars :: forall a . [IdKind] -> T a -> T a
withVars aiks ta =
--
⑨