Fixed a few bugs resulting from mandatory kind annotations for TyVars…

… & small mistakes in the CST conversion rewrite

src/Language/PureScript/CST/Convert.hs

@@ -19,9 +19,9 @@ module Language.PureScript.CST.Convert
 import Prelude hiding (take)
 
 import Control.Monad.State
-import Data.Bifunctor (bimap, first)
+import Data.Bifunctor (bimap, first, second)
 import Data.Char (toLower)
-import Data.Foldable (foldl', foldrM, toList)
+import Data.Foldable (foldl', foldrM, toList, traverse_)
 import Data.Functor (($>))
 import Data.List.NonEmpty qualified as NE
 import Data.Maybe (isJust, fromJust, mapMaybe)
@@ -43,7 +43,9 @@ import Language.PureScript.CST.Positions
 import Language.PureScript.CST.Print (printToken)
 import Language.PureScript.CST.Types
 import Data.Bitraversable (Bitraversable(..))
+import Language.PureScript.Names (runProperName, coerceProperName)
 
+import Debug.Trace (trace)
 
 type ConvertM a = State (Map Text T.SourceType) a
 
@@ -60,11 +62,43 @@ tvKind nm = do
 bindTv :: Text -> T.SourceType -> ConvertM ()
 bindTv nm ty = modify' (M.insert nm ty)
 
-reset :: ConvertM ()
-reset = modify' (\_ -> M.empty)
-
+{- Our new way of handling kinds introduces an annoying problem:
 
+   We need to have the kinds of tyvars bound the decl kind signature or
+   type signature in scope when we convert the declaration.
 
+-}
+groupSignaturesAndDeclarations :: Show a => [Declaration a] -> [[Declaration a]]
+groupSignaturesAndDeclarations decls = trace ("DECLARATIONS (grouping): " <> concatMap ((<> "\n\n") . show) decls)
+  $ foldr (go kindSigs typeSigs) [] decls'
+  where
+    -- I think this minimizes the # of traversals?
+    ((kindSigs,typeSigs),decls') = foldr (\x acc -> case x of
+        ksig@(DeclKindSignature _ _ (Labeled (nameValue -> nm) _ ty)) -> first (first $ M.insert nm ksig) acc
+        tsig@(DeclSignature _ (Labeled (nameValue -> nm) _ _)) -> first (second (M.insert nm tsig)) acc
+        other -> second (other:) acc
+      ) ((M.empty,M.empty),[]) decls
+
+    go ksigs tsigs x acc = case x of
+      dataDecl@(DeclData _ (DataHead _ (nameValue -> nm) _ ) _) -> case M.lookup nm ksigs of
+        Just sigDecl -> [sigDecl,dataDecl] : acc
+        Nothing -> [dataDecl] : acc
+      tyDecl@(DeclType _ (DataHead _ (nameValue -> nm) _) _ _) -> case M.lookup nm ksigs of
+        Just sigDecl -> [sigDecl,tyDecl] : acc
+        Nothing -> [tyDecl] : acc
+      newtypeDecl@(DeclNewtype _ (DataHead _ (nameValue -> nm) _) _ _ _) -> case M.lookup nm ksigs of
+        Just sigDecl -> [sigDecl,newtypeDecl] : acc
+        Nothing -> [newtypeDecl] : acc
+      classDecl@(DeclClass _ (clsName -> nm) _) -> case M.lookup (coerceProperName $ nameValue nm) ksigs of
+        Just sigDecl -> [sigDecl,classDecl] : acc
+        Nothing -> [classDecl] : acc
+      valDecl@(DeclValue _ (valName -> nm)) -> case M.lookup (nameValue nm) tsigs of
+        Just sigDecl -> [sigDecl,valDecl] : acc
+        Nothing -> [valDecl] : acc
+      -- I don't think anything else can have a type/kind sig but I could be wrong...
+      other -> [other] : acc
+
+
 comment :: Comment a -> Maybe C.Comment
 comment = \case
   Comment t
@@ -177,7 +211,14 @@ convertType' withinVta fileName = go
         annRec = sourceAnn fileName a a
       T.TypeApp ann (Env.tyRecord $> annRec) <$> goRow row b
     TypeForall _ kw bindings _ ty -> do
+      -- TODO: Refactor this (if it works)
       let
+        doBind (TypeVarKinded (Wrapped _ (Labeled (v, a) _ b) _)) = do
+          let nm = getIdent (nameValue a)
+          b' <- go b
+          bindTv nm b'
+        doBind (TypeVarName (v,a)) = internalError $  "Error: Universally quantified type variable without kind annotation: " <> (Text.unpack . getIdent . nameValue $ a) <> "\nat: " <> show v
+
         mkForAll a b v t = do
           let ann' = widenLeft (tokAnn $ nameTok a) $ T.getAnnForType t
           T.ForAll ann' (maybe T.TypeVarInvisible (const T.TypeVarVisible) v) (getIdent $ nameValue a) b t Nothing
@@ -188,7 +229,8 @@ convertType' withinVta fileName = go
           bindTv nm b'
           pure $ mkForAll a b' v t
         -- TODO: Fix this better
-        k (TypeVarName (v, a)) t = internalError  "forall w/o kind annotation" -- mkForAll a Nothing v
+        k (TypeVarName (v, a)) t = internalError $  "Error: Universally quantified type variable without kind annotation: " <> (Text.unpack . getIdent . nameValue $ a) <> "\nat: " <> show v
+      traverse_ doBind bindings
       inner <- go ty
       ty' <- foldrM k inner bindings
       let ann = widenLeft (tokAnn kw) $ T.getAnnForType ty'
@@ -543,6 +585,7 @@ convertBinder fileName = go
 convertDeclaration :: String -> Declaration a -> ConvertM [AST.Declaration]
 convertDeclaration fileName decl = case decl of
   DeclData _ (DataHead _ a vars) bd -> do
+    vars' <- traverse goTypeVar vars
     let
       ctrs :: SourceToken -> DataCtor a -> [(SourceToken, DataCtor a)] -> ConvertM [AST.DataConstructorDeclaration]
       ctrs st (DataCtor _ name fields) tl = do
@@ -554,7 +597,7 @@ convertDeclaration fileName decl = case decl of
             rest <- ctrs st' ctor tl'
             pure $ AST.DataConstructorDeclaration (sourceAnnCommented fileName st (nameTok name)) (nameValue name) (zip ctrFields $  fields')
                    : rest
-    vars' <- traverse goTypeVar vars
+
     ctorDecls <- maybe (pure []) (\(st, Separated hd tl) -> ctrs st hd tl) bd
     pure [AST.DataDeclaration ann Env.Data (nameValue a) vars' ctorDecls]
   DeclType _ (DataHead _ a vars) _ bd -> do
@@ -565,9 +608,9 @@ convertDeclaration fileName decl = case decl of
       vars'
       bd'
   DeclNewtype _ (DataHead _ a vars) st x ys -> do
+    vars' <- traverse goTypeVar vars
     ys' <- convertType fileName ys
     let ctrs = [AST.DataConstructorDeclaration (sourceAnnCommented fileName st (snd $ declRange decl)) (nameValue x) [(head ctrFields, ys')]]
-    vars' <- traverse goTypeVar vars
     pure [AST.DataDeclaration ann Env.Newtype (nameValue a) vars' ctrs]
   DeclClass _ (ClassHead _ sup name vars fdeps) bd -> do
     let
@@ -622,14 +665,17 @@ convertDeclaration fileName decl = case decl of
       args'
       instTy]
   DeclKindSignature _ kw (Labeled name _ ty) -> do
+    let nm =  runProperName (nameValue name)
+    ty' <- convertType fileName ty
+    bindTv nm ty'
     let
       kindFor = case tokValue kw of
         TokLowerName [] "data" -> AST.DataSig
         TokLowerName [] "newtype" -> AST.NewtypeSig
         TokLowerName [] "type" -> AST.TypeSynonymSig
         TokLowerName [] "class" -> AST.ClassSig
         tok -> internalError $ "Invalid kind signature keyword " <> Text.unpack (printToken tok)
-    pure . AST.KindDeclaration ann kindFor (nameValue name) <$> convertType fileName ty
+    pure $ [AST.KindDeclaration ann kindFor (nameValue name) ty']
   DeclSignature _ lbl ->
     pure <$> convertSignature fileName lbl
   DeclValue _ fields ->
@@ -716,8 +762,15 @@ convertDeclaration fileName decl = case decl of
         TypeUnaryRow{} -> "Row"
 
   goTypeVar = \case
-    TypeVarKinded (Wrapped _ (Labeled (_, x) _ y) _) -> (getIdent $ nameValue x,) <$>  convertType fileName y
-    TypeVarName (_, x) -> error $ "Missing kind annotation for type variable: " <> Text.unpack (getIdent $ nameValue x) -- , Nothing)
+    TypeVarKinded (Wrapped _ (Labeled (_, x) _ y) _) -> do
+      let nm = getIdent (nameValue x)
+      k <- convertType fileName y
+      bindTv nm k
+      pure (nm,k)
+    TypeVarName (_, x) -> do
+      let nm = getIdent (nameValue x)
+      ki <- tvKind nm
+      pure (nm,ki)
 
   goInstanceBinding = \case
     InstanceBindingSignature _ lbl ->
@@ -806,12 +859,13 @@ convertExport fileName export = case export of
   where
   ann = sourceSpan fileName . toSourceRange $ exportRange export
 
-convertModule :: String -> Module a ->  AST.Module
+convertModule :: Show a => String -> Module a ->  AST.Module
 convertModule fileName module'@(Module _ _ modName exps _ imps decls _) = do
   let
+    groupedDecls = groupSignaturesAndDeclarations decls
     ann = uncurry (sourceAnnCommented fileName) $ moduleRange module'
     imps' = importCtr . runConvert . convertImportDecl fileName <$> imps
-    decls' = concatMap (runConvert . convertDeclaration fileName) decls
+    decls' = concatMap (concat . runConvert . traverse (convertDeclaration fileName)) groupedDecls
     exps' = map (runConvert . convertExport fileName) . toList . wrpValue <$> exps
   uncurry AST.Module ann (nameValue modName) (imps' <> decls') exps'
   where

src/Language/PureScript/CST/Types.hs

@@ -193,14 +193,15 @@ data DataMembers a
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Generic)
 
 data Declaration a
-  = DeclData a (DataHead a) (Maybe (SourceToken, Separated (DataCtor a)))
+  =
+    DeclKindSignature a SourceToken (Labeled (Name (N.ProperName 'N.TypeName)) (Type a))
+  | DeclSignature a (Labeled (Name Ident) (Type a))
+  | DeclData a (DataHead a) (Maybe (SourceToken, Separated (DataCtor a)))
   | DeclType a (DataHead a) SourceToken (Type a)
   | DeclNewtype a (DataHead a) SourceToken (Name (N.ProperName 'N.ConstructorName)) (Type a)
   | DeclClass a (ClassHead a) (Maybe (SourceToken, NonEmpty (Labeled (Name Ident) (Type a))))
   | DeclInstanceChain a (Separated (Instance a))
   | DeclDerive a SourceToken (Maybe SourceToken) (InstanceHead a)
-  | DeclKindSignature a SourceToken (Labeled (Name (N.ProperName 'N.TypeName)) (Type a))
-  | DeclSignature a (Labeled (Name Ident) (Type a))
   | DeclValue a (ValueBindingFields a)
   | DeclFixity a FixityFields
   | DeclForeign a SourceToken SourceToken (Foreign a)

src/Language/PureScript/CoreFn/Pretty.hs

@@ -71,9 +71,6 @@ renderExpr = smartRender . asDynamic prettyValue
 renderExprStr :: Expr a -> String
 renderExprStr = T.unpack . renderExpr
 
-prettyTypeStr :: forall a. Show a => Type a -> String
-prettyTypeStr = T.unpack . smartRender . asOneLine prettyType
-
 
 {- TYPES (move later) -}
 

src/Language/PureScript/CoreFn/Pretty/Types.hs

@@ -1,4 +1,4 @@
-module Language.PureScript.CoreFn.Pretty.Types (prettyType) where
+module Language.PureScript.CoreFn.Pretty.Types (prettyType, prettyTypeStr, prettyTypeTxt) where
 
 import Prelude hiding ((<>))
 
@@ -9,7 +9,7 @@ import Control.Monad.Reader ( MonadReader(ask), Reader )
 import Language.PureScript.Environment
     ( tyRecord, tyFunction, pattern ArrayT )
 import Language.PureScript.Names (OpName(..), ProperName(..), disqualify, showQualified)
-import Language.PureScript.Types (Type (..), WildcardData (..), TypeVarVisibility (..), eqType)
+import Language.PureScript.Types (Type (..), WildcardData (..), TypeVarVisibility (..), eqType, Constraint (..))
 import Language.PureScript.PSString (prettyPrintString)
 
 import Prettyprinter
@@ -20,7 +20,7 @@ import Prettyprinter
       hcat,
       group,
       Doc,
-      Pretty(pretty) )
+      Pretty(pretty), hsep )
 import Language.PureScript.CoreFn.Pretty.Common
     ( Printer,
       LineFormat,
@@ -62,7 +62,7 @@ prettyType t  =  group <$> case t of
     HoleWildcard txt -> pure $ "?" <> pretty txt
     _ -> pure "_"
 
-  TypeConstructor _ qPropName -> pure . pretty . runProperName . disqualify $ qPropName
+  TypeConstructor _ qPropName -> pure . pretty . showQualified runProperName  $ qPropName
 
   TypeOp _ opName -> pure . pretty $ showQualified runOpName opName
 
@@ -76,7 +76,11 @@ prettyType t  =  group <$> case t of
   ForAll _ vis var mKind inner' _ -> case stripQuantifiers inner' of
     (quantified,inner) ->  goForall ([(vis,var,mKind)] <> quantified) inner
 
-  ConstrainedType _ _ _ -> error "TODO: ConstrainedType (shouldn't ever appear in Purus CoreFn)"
+  ConstrainedType _ cstrnt innertype -> do
+    cstrnt' <-  prettyConstraint cstrnt
+    inner'  <- prettyType innertype
+    pure . group $ cstrnt' <+> "=>" <+> inner'
+
 
   Skolem _ var _ i _ -> pure $ pretty var <> "#" <> pretty i
 
@@ -151,10 +155,19 @@ prettyType t  =  group <$> case t of
            pure $ Left ([],parens (pretty txt <::> k'))
          other -> Right . pure <$> prettyType other  --  error $ "Malformed row fields: \n" <> prettyTypeStr other
 
+prettyConstraint :: forall a ann. Show a => Constraint a -> Printer ann
+prettyConstraint Constraint{..} = do
+  let classNm = pretty $ showQualified runProperName constraintClass
+  argTypes <- hsep <$> traverse  prettyType constraintArgs
+  pure . group $ classNm <+> argTypes
+
 
 -- TODO For debugging, remove later
 smartRender ::  Doc ann -> Text
 smartRender = renderStrict . layoutPretty defaultLayoutOptions
 
 prettyTypeStr :: forall a. Show a => Type a -> String
 prettyTypeStr = T.unpack . smartRender . asOneLine prettyType
+
+prettyTypeTxt :: forall a. Show a => Type a -> Text
+prettyTypeTxt =  smartRender . asOneLine prettyType

src/Language/PureScript/Errors.hs

@@ -53,6 +53,7 @@ import System.Console.ANSI qualified as ANSI
 import System.FilePath (makeRelative)
 import Text.PrettyPrint.Boxes qualified as Box
 import Witherable (wither)
+import Language.PureScript.CoreFn.Pretty.Types ( prettyTypeStr )
 
 -- | A type of error messages
 data SimpleErrorMessage
@@ -1610,7 +1611,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
 
     -- If both rows are not empty, print them as diffs
     -- If verbose print all rows else only print unique rows
-    printRows :: Type a -> Type a -> (Box.Box, Box.Box)
+    printRows :: Show a => Type a -> Type a -> (Box.Box, Box.Box)
     printRows r1 r2 = case (full, r1, r2) of
       (True, _ , _) -> (printRow typeAsBox r1, printRow typeAsBox r2)
 
@@ -1689,10 +1690,10 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
   prettyDepth | full = 1000
               | otherwise = 3
 
-  prettyType :: Type a -> Box.Box
-  prettyType = prettyTypeWithDepth prettyDepth
+  prettyType :: SourceType -> Box.Box
+  prettyType = Box.text . prettyTypeStr
 
-  prettyTypeWithDepth :: Int -> Type a -> Box.Box
+  prettyTypeWithDepth :: Show a => Int -> Type a -> Box.Box
   prettyTypeWithDepth depth
     | full = typeAsBox depth
     | otherwise = typeAsBox depth .  eraseKindApps
@@ -1986,7 +1987,7 @@ renderBox = unlines
   where
   whiteSpace = all isSpace
 
-toTypelevelString :: Type a -> Maybe Box.Box
+toTypelevelString :: Show a => Type a -> Maybe Box.Box
 toTypelevelString (TypeLevelString _ s) =
   Just . Box.text $ decodeStringWithReplacement s
 toTypelevelString (TypeApp _ (TypeConstructor _ C.Text) x) =

src/Language/PureScript/Pretty/Types.hs

@@ -36,6 +36,7 @@ import Language.PureScript.PSString (PSString, prettyPrintString, decodeString)
 import Language.PureScript.Label (Label(..))
 
 import Text.PrettyPrint.Boxes (Box(..), hcat, hsep, left, moveRight, nullBox, render, text, top, vcat, (<>))
+import Language.PureScript.CoreFn.Pretty.Types (prettyTypeStr)
 
 
 data PrettyPrintType
@@ -253,8 +254,8 @@ prettyPrintTypeAtom maxDepth = render . typeAtomAsBox maxDepth
 typeAsBox' :: PrettyPrintType -> Box
 typeAsBox' = typeAsBoxImpl defaultOptions
 
-typeAsBox :: Int -> Type a -> Box
-typeAsBox maxDepth = typeAsBox' . convertPrettyPrintType maxDepth
+typeAsBox :: Show a => Int -> Type a -> Box
+typeAsBox maxDepth = text . prettyTypeStr -- typeAsBox' . convertPrettyPrintType maxDepth
 
 typeDiffAsBox' :: PrettyPrintType -> Box
 typeDiffAsBox' = typeAsBoxImpl diffOptions

src/Language/PureScript/Sugar/Names.hs

@@ -356,6 +356,7 @@ renameInModule imports (Module modSS coms mn decls exps) =
     updateType (TypeOp ann@(ss, _) name) = TypeOp ann <$> updateTypeOpName name ss
     updateType (TypeConstructor ann@(ss, _) name) = TypeConstructor ann <$> updateTypeName name ss
     updateType (ConstrainedType ann c t) = ConstrainedType ann <$> updateInConstraint c <*> pure t
+    updateType (TypeVar ann nm ki) = TypeVar ann nm <$> updateType ki
     updateType t = return t
     updateInConstraint :: SourceConstraint -> m SourceConstraint
     updateInConstraint (Constraint ann@(ss, _) name ks ts info) =

src/Language/PureScript/TypeChecker/Kinds.hs

@@ -58,6 +58,7 @@ import Language.PureScript.Types
 import Language.PureScript.Pretty.Types (prettyPrintType)
 import Language.PureScript.CST.Types (Comment)
 
+
 -- TODO/REVIEW/HACK: -----------------------------------
 -- NO CLUE IF THE CHANGES I MADE HERE ARE CORRECT
 generalizeUnknowns :: [(Unknown, SourceType)] -> SourceType -> SourceType
@@ -190,10 +191,10 @@ inferKind = \tyToInfer ->
       pure (ty, E.kindSymbol $> ann)
     ty@(TypeLevelInt ann _) ->
       pure (ty, E.tyInt $> ann)
-    ty@(TypeVar ann v ki) -> do
-      moduleName <- unsafeCheckCurrentModule
-      kind <- apply =<< lookupTypeVariable moduleName (Qualified ByNullSourcePos $ ProperName v)
-      pure (ty, kind $> ann)
+    ty@(TypeVar ann v kx) -> do
+      -- moduleName <- unsafeCheckCurrentModule
+      -- kind <- apply =<< lookupTypeVariable moduleName (Qualified ByNullSourcePos $ ProperName v)
+      pure (ty, kx $> ann)
     ty@(Skolem ann _ mbK _ _) -> do
       kind <- apply $  mbK
       pure (ty, kind $> ann)
@@ -218,7 +219,7 @@ inferKind = \tyToInfer ->
     KindApp ann t1 t2 -> do
       (t1', kind) <- bitraverse pure apply =<< go t1
       case kind of
-        ForAll _ _ arg (argKind) resKind _ -> do
+        ForAll _ _ arg argKind resKind _ -> do
           t2' <- checkKind t2 argKind
           pure (KindApp ann t1' t2', replaceTypeVars arg t2' resKind)
         _ ->
@@ -529,10 +530,10 @@ elaborateKind = \case
         throwError . errorMessage' (fst ann) . UnknownName . fmap TyName $ v
       Just (kind, _) ->
         ($> ann) <$> apply kind
-  TypeVar ann a ki -> do
-    moduleName <- unsafeCheckCurrentModule
-    kind <- apply =<< lookupTypeVariable moduleName (Qualified ByNullSourcePos $ ProperName a)
-    unifyKinds ki kind -- TODO/REVIEW/HACK: I DO NOT KNOW WHETHER THIS IS WHAT WE WANT
+  TypeVar ann a kind -> do
+    -- moduleName <- unsafeCheckCurrentModule
+    -- kind <- apply =<< lookupTypeVariable moduleName (Qualified ByNullSourcePos $ ProperName a)
+    -- unifyKinds ki kind -- TODO/REVIEW/HACK: I DO NOT KNOW WHETHER THIS IS WHAT WE WANT
     pure (kind $> ann)
   (Skolem ann _ mbK _ _) -> do
     kind <- apply $  mbK

src/Language/PureScript/TypeChecker/Unify.hs

@@ -128,7 +128,7 @@ unifyTypes t1 t2 = do
     sk `unifyTypes` ty2
   unifyTypes' ForAll{} _ = internalError "unifyTypes: unspecified skolem scope"
   unifyTypes' ty f@ForAll{} = f `unifyTypes` ty
-  unifyTypes' (TypeVar _ v1 k1) (TypeVar _ v2 k2) | v1 == v2 = unifyTypes k1 k2  -- REVIEW/HACK: Not sure if this is right...
+  unifyTypes' (TypeVar _ v1 k1) (TypeVar _ v2 k2) | v1 == v2 = pure () -- unifyTypes k1 k2  -- REVIEW/HACK: Not sure if this is right...
   unifyTypes' ty1@(TypeConstructor _ c1) ty2@(TypeConstructor _ c2) =
     guardWith (errorMessage (TypesDoNotUnify ty1 ty2)) (c1 == c2)
   unifyTypes' (TypeLevelString _ s1) (TypeLevelString _ s2) | s1 == s2 = return ()