fix mask kind inference

koka-lang · Feb 12, 2024 · bb6c56b · bb6c56b
1 parent fe31505
commit bb6c56b
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 25 deletions.
diff --git a/src/Kind/Infer.hs b/src/Kind/Infer.hs
@@ -485,24 +485,25 @@ infResolveX tp ctx rng
        skind <- subst ikind
        -- allow also effect label constructors without giving type parameters
        let (kargs,kres) = infExtractKindFun skind
-       if (not (null kargs))
-        then let vars     = [(newName ("_" ++ show i)) | (_,i) <- zip kargs [1..]]
-                 quals    = map (\(name) -> TypeBinder name KindNone rng rng) vars
-                 tpvars   = map (\(name) -> TpVar name rng) vars
-                 newtp    = foldr (\q t -> TpQuan QSome q t rng) (TpApp tp tpvars rng) quals
-             in infResolveX newtp ctx rng -- recurse..
-       -- auto upgrade bare labels of HX or HX1 to X kind labels.
-        else do effect <- case skind of
-                            KICon kind | kind == kindLabel   -> return infTp
-                            KICon kind | isKindHandled kind
-                              -> do linear <- checkLinearEffect infTp
-                                    return $ (if linear then makeHandled1 else makeHandled) infTp rng
-
-                            -- KICon kind | isKindHandled kind  -> return (makeHandled infTp rng)
-                            ---KICon kind | isKindHandled1 kind -> return (makeHandled1 infTp rng)
-                            _ -> do unify ctx rng infKindLabel skind
-                                    return infTp
-                resolveType M.empty False effect
+       if (length kargs > 2)
+         then let vars     = [(newName ("_" ++ show i)) | i <- [1..(length kargs - 2)]]
+                  quals    = map (\(name) -> TypeBinder name KindNone rng rng) vars
+                  tpvars   = map (\(name) -> TpVar name rng) vars
+                  newtp    = foldr (\q t -> TpQuan QSome q t rng) (TpApp tp tpvars rng) quals
+              in infResolveX newtp ctx rng -- recurse..
+         else -- auto upgrade bare labels of HX or HX1 to X kind labels.
+              do  effect <- case skind of
+                              KICon kind | kind == kindLabel   -> return infTp
+                              KICon kind | isKindHandled kind
+                                -> do linear <- checkLinearEffect infTp
+                                      return $ (if linear then makeHandled1 else makeHandled) infTp rng
+
+                              -- KICon kind | isKindHandled kind  -> return (makeHandled infTp rng)
+                              ---KICon kind | isKindHandled1 kind -> return (makeHandled1 infTp rng)
+                              _ -> do trace ("infResolveX: " ++ show tp ++ ": " ++ show skind) $
+                                        unify ctx rng infKindLabel skind
+                                      return infTp
+                  resolveType M.empty False effect
 
 
 
@@ -611,7 +612,7 @@ infExpr expr
                                    ops' <- mapM infHandlerBranch ops
                                    return (Handler hsort scoped override allowMask meff' pars' reinit' ret' final' ops' hrng rng)
       Inject tp expr b range-> do expr' <- infExpr expr
-                                  tp'   <- infResolveX tp (Check "Can only inject effect constants (of kind X)" range) range
+                                  tp'   <- infResolveX tp (Check "Can only inject effect constants (of kind X)" range) (getRange tp)
                                   -- trace ("resolve ann: " ++ show (pretty tp')) $
                                   return (Inject tp' expr' b range)
 
@@ -793,8 +794,8 @@ checkLinearEffect utp
       TpCon name rng  -> do mbInfo <- lookupDataInfo name
                             case mbInfo of
                               Just info | dataDefIsLinear (dataInfoDef info)
-                                        -> trace ("found linear effect: " ++ show name) $ return True
-                              _         -> return False
+                                 -> return True
+                              _  -> return False
       _               -> return False
 
 infParam expected context (name,tp)

diff --git a/src/Kind/InferKind.hs b/src/Kind/InferKind.hs
@@ -15,6 +15,7 @@ module Kind.InferKind ( InfKind(..)
                       , ppInfKind, niceInfKinds
                       , infExtractKindFun
                       , isInfKindScope
+                      , isInfKindHandled
 
                       , InfKGamma
 
@@ -92,7 +93,15 @@ infExtractKindFun infkind
       KICon (KApp (KApp kindArrow k1) k2)   -> inj (KICon k1) (infExtractKindFun (KICon k2))
       _  -> ([],infkind)
   where
-    inj k1 (ks,k) = (k1:ks,k1)
+    inj k1 (ks,k) = (k1:ks,k)
+
+
+isInfKindHandled :: InfKind -> Bool
+isInfKindHandled ikind
+  = case infExtractKindFun ikind of
+      ([KICon k1, KICon k2], KICon k3) -> isKindHandled (kindFun k1 (kindFun k2 k3))
+      _ -> False
+
 
 {---------------------------------------------------------------
   Substitution

diff --git a/src/Syntax/Parse.hs b/src/Syntax/Parse.hs
@@ -2204,9 +2204,9 @@ injectType
  = do rng1 <- keywordInject
       behind <- do { specialId "behind" <|> specialId "other"; return True } <|> return False
       langle
-      tp <- ptype
-      rangle
-      return (rng1, \exp -> Inject (promoteType tp) exp behind (combineRanged rng1 exp))
+      tp   <- ptype
+      rng2 <- rangle
+      return (rng1, \exp -> Inject (promoteType tp) exp behind (combineRanged rng1 rng2))
       {-
       tps1 <- sepBy1 ptype comma
       rng2 <- rangle