shithub: MicroHs

Download patch

ref: 7413420cb26bf029aa31cc7f8188171b52dff8fd
parent: 1025e8b860cee9258574004abbca39e42abdee3e
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Wed Oct 18 12:58:35 EDT 2023 

More class stuff.


--- a/comb/mhs.comb
+++ b/comb/mhs.comb
@@ -1,3 +1,3 @@
 v4.0
-1007
-((A :0 _891) ((A :1 ((B _937) _0)) ((A :2 (((S' _937) _0) I)) ((A :3 _861) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _890) ((C _75) _5))) ((A :7 (((C' _6) (_908 _72)) ((_75 _906) _71))) ((A :8 ((B ((S _937) _906)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_75 _190)) _10)) ((A :12 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_74 _9)) P)) ((A :15 ((B (B (_74 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_74 _9)) (B (P _819)))) ((A :19 ((B (_74 _9)) (BK (P _819)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _115)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _116)))))) ((A :23 ((B Y) ((B (B (P (_14 _819)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _819))) ((A :26 (_22 _76)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 _866) ((A :36 _867) ((A :37 (((S' _28) (_858 #97)) ((C _858) #122))) ((A :38 (((S' _28) (_858 #65)) ((C _858) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_858 #48)) ((C _858) #57))) ((A :41 (((S' _28) (_858 #32)) ((C _858) #126))) ((A :42 _855) ((A :43 _856) ((A :44 _858) ((A :45 _857) ((A :46 (((S' _27) ((C _42) #32)) (((S' _27) ((C _42) #9)) ((C _42) #10)))) ((A :47 ((S ((S (((S' _28) (_44 #65)) ((C _44) #90))) (_34 (((_817 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_817 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _826) ((A :50 _827) ((A :51 _828) ((A :52 _829) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _830) ((A :59 _831) ((A :60 _58) ((A :61 _59) ((A :62 _832) ((A :63 _833) ((A :64 _834) ((A :65 _835) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _836) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 B) ((A :76 I) ((A :77 K) ((A :78 C) ((A :79 _862) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _820) ((A :83 _821) ((A :84 _822) ((A :85 _823) ((A :86 _824) ((A :87 _825) ((A :88 (_83 #0)) ((A :89 _843) ((A :90 _844) ((A :91 _845) ((A :92 _846) ((A :93 _847) ((A :94 _848) ((A :95 _89) ((A :96 (BK K)) ((A :97 ((B BK) ((B (B BK)) P))) ((A :98 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :99 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_92 #0))) (_89 #0)))) ((B (B ((C' P) (_87 #1)))) _82))) (C P))) _85)) _86)) ((A :100 _96) ((A :101 (((S' C) ((B (P _178)) (((C' (C' B)) (((C' C) _89) _178)) _179))) ((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') (_89 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_89 #1)))) ((B ((C' C) ((B ((C' S') (_89 #2))) (C _101)))) (C _101))))) (C _101))))) (C _101)))) (T K))) (T A)))) ((C _99) #4)))) ((A :102 (_108 _77)) ((A :103 ((_123 (_80 _102)) _100)) ((A :104 ((C (((C' B) ((P _115) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _105)))) (((S' (C' (C' B))) ((B (B (B _105))) (((S' (C' B)) ((B (B _105)) (((C' B) ((B _121) (T #0))) _104))) (((C' B) ((B _121) (T #1))) _104)))) (((C' B) ((B _121) (T #2))) _104)))) (((C' B) ((B _121) (T #3))) _104)))) ((B T) ((B (B P)) ((C' _82) (_84 #4)))))) ((A :105 ((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) _91)))) ((B ((C' B) _116)) _105)))))) ((B ((C' B) _116)) (C _105)))))))))) (((_817 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :106 ((_75 (_121 _190)) _104)) ((A :107 (((C' C) (((C' C) (C _101)) (_3 "Data.IntMap.!"))) I)) ((A :108 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B
\ No newline at end of file
+1009
+((A :0 _893) ((A :1 ((B _939) _0)) ((A :2 (((S' _939) _0) I)) ((A :3 _863) ((A :4 (_3 "undefined")) ((A :5 I) ((A :6 (((C' B) _892) ((C _75) _5))) ((A :7 (((C' _6) (_910 _72)) ((_75 _908) _71))) ((A :8 ((B ((S _939) _908)) _3)) ((A :9 T) ((A :10 (T I)) ((A :11 ((B (_75 _190)) _10)) ((A :12 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (B _10)))) ((A :13 ((B (B (_74 _9))) (((C' B) ((B C) _10)) (BK _10)))) ((A :14 ((B (_74 _9)) P)) ((A :15 ((B (B (_74 _9))) ((B ((C' C) _10)) (B P)))) ((A :16 _15) ((A :17 (((C' B) _12) (((C' B) _12) (B _14)))) ((A :18 ((B (_74 _9)) (B (P _821)))) ((A :19 ((B (_74 _9)) (BK (P _821)))) ((A :20 ((_74 _9) ((S P) I))) ((A :21 ((B (_74 _9)) ((C (S' P)) I))) ((A :22 ((B Y) ((B (B (P (_14 _115)))) (((C' B) ((B (C' B)) (B _12))) (((C' (C' B)) (B _12)) ((B (B _14)) _116)))))) ((A :23 ((B Y) ((B (B (P (_14 _821)))) ((B (C' B)) (B _13))))) ((A :24 _3) ((A :25 (T (_14 _821))) ((A :26 (_22 _76)) ((A :27 (R _34)) ((A :28 (T _33)) ((A :29 ((P _34) _33)) ((A :30 _34) ((A :31 ((C ((C S') _29)) I)) ((A :32 ((C S) _29)) ((A :33 K) ((A :34 A) ((A :35 _868) ((A :36 _869) ((A :37 (((S' _28) (_860 #97)) ((C _860) #122))) ((A :38 (((S' _28) (_860 #65)) ((C _860) #90))) ((A :39 (((S' _27) _37) _38)) ((A :40 (((S' _28) (_860 #48)) ((C _860) #57))) ((A :41 (((S' _28) (_860 #32)) ((C _860) #126))) ((A :42 _857) ((A :43 _858) ((A :44 _860) ((A :45 _859) ((A :46 (((S' _27) ((C _42) #32)) (((S' _27) ((C _42) #9)) ((C _42) #10)))) ((A :47 ((S ((S (((S' _28) (_44 #65)) ((C _44) #90))) (_34 (((_819 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #65))) (_36 #97))))) ((A :48 ((S ((S (((S' _28) (_44 #97)) ((C _44) #97))) (_34 (((_819 "lib/Data/Char.hs") #3) #8)))) ((B _35) (((C' _82) (((C' _83) _36) (_36 #97))) (_36 #65))))) ((A :49 _828) ((A :50 _829) ((A :51 _830) ((A :52 _831) ((A :53 (_50 %0.0)) ((A :54 _49) ((A :55 _50) ((A :56 _51) ((A :57 _52) ((A :58 _832) ((A :59 _833) ((A :60 _58) ((A :61 _59) ((A :62 _834) ((A :63 _835) ((A :64 _836) ((A :65 _837) ((A :66 _62) ((A :67 _63) ((A :68 _64) ((A :69 _65) ((A :70 _838) ((A :71 ((B BK) T)) ((A :72 (BK T)) ((A :73 P) ((A :74 I) ((A :75 B) ((A :76 I) ((A :77 K) ((A :78 C) ((A :79 _864) ((A :80 ((C ((C S') _190)) _191)) ((A :81 (((C' (S' (C' B))) B) I)) ((A :82 _822) ((A :83 _823) ((A :84 _824) ((A :85 _825) ((A :86 _826) ((A :87 _827) ((A :88 (_83 #0)) ((A :89 _845) ((A :90 _846) ((A :91 _847) ((A :92 _848) ((A :93 _849) ((A :94 _850) ((A :95 _89) ((A :96 (BK K)) ((A :97 ((B BK) ((B (B BK)) P))) ((A :98 ((B (B (B BK))) ((B (B (B BK))) ((B (B (B C))) ((B (B C)) P))))) ((A :99 (((S' S) (((S' (S' C)) (((C' (C' S)) (((C' B) ((B (S' S')) (((C' B) ((B _27) (_92 #0))) (_89 #0)))) ((B (B ((C' P) (_87 #1)))) _82))) (C P))) _85)) _86)) ((A :100 _96) ((A :101 (((S' C) ((B (P _178)) (((C' (C' B)) (((C' C) _89) _178)) _179))) ((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') (_89 #0))))) ((B ((C' (C' C)) ((B (B ((S' S') (_89 #1)))) ((B ((C' C) ((B ((C' S') (_89 #2))) (C _101)))) (C _101))))) (C _101))))) (C _101)))) (T K))) (T A)))) ((C _99) #4)))) ((A :102 (_108 _77)) ((A :103 ((_123 (_80 _102)) _100)) ((A :104 ((C (((C' B) ((P _115) (((C' (C' O)) P) K))) (((S' (C' (C' (C' B)))) ((B (B (B (B _105)))) (((S' (C' (C' B))) ((B (B (B _105))) (((S' (C' B)) ((B (B _105)) (((C' B) ((B _121) (T #0))) _104))) (((C' B) ((B _121) (T #1))) _104)))) (((C' B) ((B _121) (T #2))) _104)))) (((C' B) ((B _121) (T #3))) _104)))) ((B T) ((B (B P)) ((C' _82) (_84 #4)))))) ((A :105 ((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) _91)))) ((B ((C' B) _116)) _105)))))) ((B ((C' B) _116)) (C _105)))))))))) (((_819 "lib/Data/IntMap.hs") #3) #8))))))))) ((A :106 ((_75 (_121 _190)) _104)) ((A :107 (((C' C) (((C' C) (C _101)) (_3 "Data.IntMap.!"))) I)) ((A :108 ((B ((C' B) T)) ((B (B Y)) (((C' (C' (S' (S' C)))) ((B
\ No newline at end of file
--- a/src/MicroHs/Ident.hs
+++ b/src/MicroHs/Ident.hs
@@ -80,6 +80,7 @@
     case dropWhile (neChar '.') s of
       "" -> s
       '.':r -> unQualString r
+      _ -> undefined -- This cannot happen, but GHC doesn't know that
   else
     s
 
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -372,9 +372,9 @@
   is <- gets instances
   putInstances (ic : is)
 
-addConstraint :: (Ident, EConstraint) -> T ()
-addConstraint e = T.do
-  traceM (show e)
+addConstraint :: String -> (Ident, EConstraint) -> T ()
+addConstraint msg e@(d, ctx) = T.do
+--  traceM $ "addConstraint: " ++ msg ++ " " ++ showIdent d ++ " :: " ++ showEType ctx
   TC mn n fx tt st vt ast sub m cs is es <- get
   put $ TC mn n fx tt st vt ast sub m cs is (e : es)
 
@@ -621,7 +621,7 @@
 tcReset :: T ()
 tcReset = T.do
   TC mn u fx tenv senv venv ast _ m cs is es <- get
-  put (TC mn 0 fx tenv senv venv ast IM.empty m cs is es)
+  put (TC mn u fx tenv senv venv ast IM.empty m cs is es)
 
 newUVar :: T EType
 newUVar = EUVar <$> newUniq
@@ -635,6 +635,11 @@
   put (seq n' $ TC mn n' fx tenv senv venv ast sub m cs is es)
   T.return n
 
+newIdent :: SLoc -> String -> T Ident
+newIdent loc s = T.do
+  u <- newUniq
+  T.return $ mkIdentSLoc loc $ s ++ "$" ++ showInt u
+
 tLookup :: --XHasCallStack =>
            String -> String -> Ident -> T (Expr, EType)
 tLookup msg0 msgN i = T.do
@@ -641,7 +646,7 @@
   env <- gets valueTable
   case M.lookup i env of
     Nothing -> tcError (getSLocIdent i) $ msg0 ++ ": " ++ showIdent i
-               -- ++ "\n" ++ show env ;
+               -- ++ "\n" ++ show (map (unIdent . fst) (M.toList env))
     Just [Entry e s] -> T.return (setSLocExpr (getSLocIdent i) e, s)
     Just _ -> tcError (getSLocIdent i) $ msgN ++ ": " ++ showIdent i
 
@@ -672,7 +677,8 @@
 tDict (EApp (EApp (EVar (Ident loc "Primitives.=>")) ctx) t) = T.do
   u <- newUniq
   let d = mkIdentSLoc loc ("dict$" ++ showInt u)
-  addConstraint (d, ctx)
+  --traceM $ "addConstraint: " ++ showIdent d ++ " :: " ++ showEType ctx
+  addConstraint "from tDict " (d, ctx)
   tDict t
 tDict t = T.return t
 
@@ -994,10 +1000,10 @@
 --  * Add instance to instance table
 expandInst :: EDef -> T [EDef]
 expandInst dinst@(Instance vks ctx cc bs) = T.do
-  let loc@(SLoc _ l c) = getSLocExpr cc
+  let loc = getSLocExpr cc
       iCls = getAppCon cc
-      iInst = mkIdentSLoc loc $ "inst$L" ++ showInt l ++ "C" ++ showInt c
-      sign = Sign iInst (eForall vks cc)
+  iInst <- newIdent loc "inst"
+  let sign = Sign iInst (eForall vks cc)
   (e, _) <- tLookupV iCls
   ct <- gets classTable
   let qiCls = getAppCon e
@@ -1018,7 +1024,8 @@
       sups = replicate nsup (EVar $ mkIdentSLoc loc "dict$")
       args = sups ++ meths
   let bind = Fcn iInst [Eqn [] $ EAlts [([], foldl EApp (EVar $ mkClassConstructor iCls) args)] bs']
-  addInstance (iInst, vks, ctx, cc)
+  mn <- gets moduleName
+  addInstance (qualIdent mn iInst, vks, ctx, cc)
   T.return [dinst, sign, bind]
 expandInst d = T.return [d]
 
@@ -1063,11 +1070,23 @@
       methTys = map (\ (BSign _ t) -> t) meths
       supTys = ctx  -- XXX should do some checking
       targs = supTys ++ methTys
-      tret = tApps iCls (map tVarK vks)
+      qiCls = qualIdent mn iCls
+      tret = tApps qiCls (map tVarK vks)
       cti = [ (qualIdent mn iCon, length targs) ]
       iCon = mkClassConstructor iCls
   extValETop iCon (EForall vks $ foldr tArrow tret targs) (ECon $ ConData cti (qualIdent mn iCon))
+  let addMethod (BSign i t) = extValETop i (EForall vks $ tApps qiCls (map (EVar . idKindIdent) vks) `tImplies` t) (EVar i)
+      addMethod _ = impossible
+--  traceM ("addValueClass " ++ showEType (ETuple ctx))
+  T.mapM_ addMethod meths
 
+{-
+bundleConstraints :: [EConstraint] -> EType -> EType
+bundleConstraints []  t = t
+bundleConstraints [c] t = tImplies c t
+bundleConstraints cs  t = tImplies (ETuple cs) t
+-}
+
 mkClassConstructor :: Ident -> Ident
 mkClassConstructor i = addIdentSuffix i "$C"
 
@@ -1082,11 +1101,10 @@
     Fcn i eqns -> T.do
       (_, tt) <- tLookup "no type signature" "many type signatures" i
       let (iks, tfn) = unForall tt
-      traceM $ "tcDefValue: " ++ show i ++ " :: " ++ showExpr tt
+--      traceM $ "tcDefValue: " ++ showIdent i ++ " :: " ++ showExpr tt
       mn <- gets moduleName
       teqns <- withExtTyps iks $ tcEqns tfn eqns
 --      traceM (showEDefs [Fcn i eqns, Fcn i teqns])
-      _ <- solveConstraints
       T.return $ Fcn (qualIdent mn i) teqns
     ForImp ie i t -> T.do
       mn <- gets moduleName
@@ -1141,6 +1159,7 @@
 tCheckExpr :: --XHasCallStack =>
               EType -> Expr -> T Expr
 tCheckExpr t e | Just (ctx, t') <- getImplies t = T.do
+  _ <- undefined -- XXX
   u <- newUniq
   let d = mkIdentSLoc (getSLocExpr e) ("adict$" ++ showInt u)
   e' <- withDict (d, [], [], ctx) $ tCheckExpr t' e
@@ -1217,6 +1236,14 @@
                   _ -> impossible
                 T.return p
           
+        _ | eqIdent i (mkIdent "dict$") -> T.do
+          -- Magic variable that just becomes the dictionary
+          d <- newIdent (getSLocIdent i) "dict$"
+          case mt of
+            Infer _ -> impossible
+            Check t -> addConstraint "from dict$" (d, t)
+          T.return (EVar d)
+
         _ -> T.do
           -- Type checking an expression (or type)
           T.when (isDummyIdent i) impossible
@@ -1236,6 +1263,7 @@
       (f', ft) <- tInferExpr f
       (at, rt) <- unArrow loc ft
       tcm <- gets tcMode
+--      traceM ("tcExpr EApp: " ++ showExpr f ++ " :: " ++ showEType ft)
       case tcm of
         TCPat -> T.do
           a' <- tCheckExpr at a
@@ -1440,6 +1468,16 @@
     T.return (ELam ps er)
 
 tcEqns :: EType -> [Eqn] -> T [Eqn]
+tcEqns t eqns | Just (ctx, t') <- getImplies t = T.do
+  let loc = getSLocExpr $ ELet [BFcn dummyIdent eqns] (EVar dummyIdent)
+  d <- newIdent loc "adict"
+  f <- newIdent loc "fcn"
+  eqns' <- withDict (d, [], [], ctx) $ T.do
+    es <- tcEqns t' eqns
+    _ <- solveConstraints
+    T.return es
+  let eqn = Eqn [EVar d] $ EAlts [([], EVar f)] [BFcn f eqns']
+  T.return [eqn]
 tcEqns t eqns = T.mapM (tcEqn t) eqns
 
 tcEqn :: EType -> Eqn -> T Eqn
@@ -1454,6 +1492,7 @@
   tcBinds bs $ \ bbs -> T.do { aalts <- T.mapM (tcAlt tt) alts; T.return (EAlts aalts bbs) }
 
 tcAlt :: EType -> EAlt -> T EAlt
+--tcAlt t _ | trace ("tcAlt: " ++ showExpr t) False = undefined
 tcAlt t (ss, rhs) = tcGuards ss $ \ sss -> T.do { rrhs <- tCheckExpr t rhs; T.return (sss, rrhs) }
 
 tcGuards :: forall a . [EStmt] -> ([EStmt] -> T a) -> T a
@@ -1743,7 +1782,9 @@
       tcErrorTK (getSLocExpr expr) "not polymorphic enough"
     T.return expr'
 
-subsCheckRho :: SLoc -> Sigma -> Rho -> T ()
+subsCheckRho :: --XHasCallStack =>
+                SLoc -> Sigma -> Rho -> T ()
+--subsCheckRho _ t1 t2 | trace ("subsCheckRho: " ++ showEType t1 ++ " = " ++ showEType t2) False = undefined
 subsCheckRho loc sigma1@(EForall _ _) rho2 = T.do -- Rule SPEC
   rho1 <- tInst sigma1
   subsCheckRho loc rho1 rho2
@@ -1761,7 +1802,8 @@
   subsCheck loc a2 a1
   subsCheckRho loc r1 r2
 
-instSigma :: SLoc -> Sigma -> Expected -> T ()
+instSigma :: --XHasCallStack =>
+             SLoc -> Sigma -> Expected -> T ()
 instSigma loc t1 (Check t2) = subsCheckRho loc t1 t2
 instSigma _   t1 (Infer r) = T.do
   t1' <- tInst t1
@@ -1775,6 +1817,9 @@
   if null cs then
     T.return ()
    else T.do
-    traceM "solveConstraints"
-    traceM (unlines $ map (\ (i, t) -> showIdent i ++ " :: " ++ showExpr t) cs)
+--    traceM "solveConstraints"
+    cs' <- T.mapM (\ (i,t) -> T.do { t' <- derefUVar t; T.return (i,t') }) cs
+--    traceM ("constraints:\n" ++ unlines (map (\ (i, t) -> showIdent i ++ " :: " ++ showExpr t) cs'))
+    is <- gets instances
+--    traceM ("instances:\n" ++ unlines (map (\ (i, _, _, t) -> showIdent i ++ " :: " ++ showExpr t) is))
     T.return ()
-- 
⑨