Fixed mutual recursion bug in declToCoreFn, removed let generalizatio…

…n machinery

src/Language/PureScript/CoreFn/Desugar.hs

@@ -1,14 +1,11 @@
 {- HLINT ignore "Use void" -}
 {- HLINT ignore "Use <$" -}
 {-# LANGUAGE TypeApplications #-}
-
 module Language.PureScript.CoreFn.Desugar(moduleToCoreFn) where
 
 import Prelude
 import Protolude (ordNub, orEmpty, zipWithM, MonadError (..), Foldable (toList))
 
-
-
 import Data.Maybe (mapMaybe)
 import Data.List.NonEmpty qualified as NEL
 import Data.Map qualified as M
@@ -60,7 +57,7 @@ import Language.PureScript.Types (
   SourceType,
   Type(..),
   srcTypeConstructor,
-  srcTypeVar, srcTypeApp, quantify, eqType, srcRCons, unknowns, everywhereOnTypesM)
+  srcTypeVar, srcTypeApp, quantify, eqType, srcRCons, unknowns, everywhereOnTypesM, containsUnknowns)
 import Language.PureScript.AST.Binders qualified as A
 import Language.PureScript.AST.Declarations qualified as A
 import Language.PureScript.AST.SourcePos qualified as A
@@ -124,7 +121,9 @@ import Language.PureScript.CoreFn.Desugar.Utils
       toReExportRef,
       traverseLit,
       wrapTrace,
-      M )
+      traceNameTypes,
+      M,
+      )
 import Text.Pretty.Simple (pShow)
 import Data.Text.Lazy qualified as LT
 
@@ -221,18 +220,20 @@ declToCoreFn  mn (A.ValueDecl (ss, _) name _ _ [A.MkUnguarded e]) = wrapTrace ("
       pure [NonRec (ssA ss) name expr]
 -- Recursive binding groups. This is tricky. Calling `typedOf` saves us a lot of work, but it's hard to tell whether that's 100% safe here
 declToCoreFn  mn (A.BindingGroupDeclaration ds) = wrapTrace "declToCoreFn BINDING GROUP" $ do
-  let stripped :: [((A.SourceAnn, Ident), A.Expr)] = NE.toList $  (\(((ss, com), name), _, e) -> (((ss, com), name), e)) <$> ds
-  types <- typesOf RecursiveBindingGroup mn stripped -- NOTE: If something weird breaks, look here. It's possible that `typesOf` makes calls to type CHECKING machinery that we don't want to ever invoke.
-  recBody <- bindLocalVariables (prepareBind <$> types) $ traverse goRecBindings types
+  let typed  = NE.toList $ extractTypeAndPrepareBind <$> ds
+      toBind = snd <$> typed
+  recBody <- bindLocalVariables toBind $ traverse goRecBindings typed
   pure [Rec recBody]
  where
-   prepareBind :: ((A.SourceAnn, Ident), (A.Expr, SourceType)) -> (SourceSpan, Ident, SourceType, NameVisibility)
-   prepareBind (((ss',_),ident),(_,sty)) = (ss',ident,sty,Defined)
-
-   goRecBindings ::  ((A.SourceAnn, Ident), (A.Expr, SourceType)) -> m ((Ann, Ident), Expr Ann)
-   goRecBindings ((ann,ident),(expr,ty)) = do
-     expr' <- exprToCoreFn mn (fst ann) (Just ty) expr
-     pure ((ssA $ fst ann,ident), expr')
+   -- If we only ever call this on a top-level binding group then this should be OK, all the exprs should be explicitly typed
+   extractTypeAndPrepareBind :: ((A.SourceAnn, Ident), NameKind,  A.Expr) -> (A.Expr, (SourceSpan,Ident,SourceType,NameVisibility))
+   extractTypeAndPrepareBind (((ss',_),ident),_,A.TypedValue _ e ty) = (e,(ss',ident,ty,Defined))
+   extractTypeAndPrepareBind (((ss',_),ident),_,_) = error $ "Top level declaration " <> (showIdent' ident) <> " should have a type annotation, but does not"
+
+   goRecBindings :: (A.Expr, (SourceSpan,Ident,SourceType,NameVisibility)) -> m ((Ann, Ident), Expr Ann)
+   goRecBindings (expr,(ss',ident,ty,nv)) = do
+     expr' <- exprToCoreFn mn ss' (Just ty) expr
+     pure ((ssA ss',ident), expr')
 -- TODO: Avoid catchall case
 declToCoreFn _ _ = pure []
 
@@ -281,6 +282,7 @@ exprToCoreFn mn _ (Just t) (A.Abs (A.VarBinder ssb name) v) = wrapTrace ("exprTo
       pure . f $ Abs (ssA ssb) (purusFun a b) name body
     other -> error $ "Invalid function type " <> ppType 100 other
 -- By the time we receive the AST, only Lambdas w/ a VarBinder should remain
+-- TODO: Better failure message if we pass in 'Nothing' as the (Maybe Type) arg for an Abstraction
 exprToCoreFn _  _ t lam@(A.Abs _ _) =
   internalError $ "Abs with Binder argument was not desugared before exprToCoreFn mn: \n" <> show lam <> "\n\n" <> show (const () <$> t)
 -- Ad hoc machinery for handling desugared type class dictionaries. As noted above, the types "lie" in generated code.
@@ -445,6 +447,8 @@ altToCoreFn  mn ss ret boundTypes (A.CaseAlternative bs vs) = wrapTrace "altToCo
    weirder cases in the AST. We'll have to deal with any problems once we have examples that
    clearly isolate the problematic syntax nodes.
 -}
+-- TODO: Figure out why exprs in a valuedec are a list, maybe fix?
+-- TODO: Trees that grow (paper)
 transformLetBindings :: forall m. M m => ModuleName -> SourceSpan -> [Bind Ann] -> [A.Declaration] -> A.Expr -> m ([Bind Ann], Expr Ann)
 transformLetBindings mn ss seen [] ret = (seen,) <$> withBindingGroupVisible (exprToCoreFn mn ss Nothing ret)
 transformLetBindings mn _ss seen ((A.ValueDecl sa@(ss,_) ident nameKind [] [A.MkUnguarded (A.TypedValue checkType val ty)]) : rest) ret =
@@ -453,51 +457,35 @@ transformLetBindings mn _ss seen ((A.ValueDecl sa@(ss,_) ident nameKind [] [A.Mk
     thisDecl <- declToCoreFn mn (A.ValueDecl sa ident nameKind [] [A.MkUnguarded (A.TypedValue checkType val ty)])
     let seen' = seen ++ thisDecl
     transformLetBindings mn _ss seen' rest ret
+-- TODO: Write a question where I ask what can legitimately be inferred as a type in a let binding context
 transformLetBindings mn _ss seen (A.ValueDecl sa@(ss,_) ident nameKind [] [A.MkUnguarded val] : rest) ret = wrapTrace ("transformLetBindings VALDEC " <> showIdent' ident <> " = " <> renderValue 100 val) $ do
-  _ty <- inferType Nothing val {- FIXME: This sometimes gives us a type w/ unknowns, but we don't have any other way to get at the type -}
-  ty <- generalizeUnknowns _ty
-  bindNames (M.singleton (Qualified (BySourcePos $ spanStart ss) ident) (ty, nameKind, Defined)) $ do
-    thisDecl <- declToCoreFn mn (A.ValueDecl sa ident nameKind [] [A.MkUnguarded (A.TypedValue False val ty)])
-    let seen' = seen ++ thisDecl
-    transformLetBindings mn _ss seen' rest ret
+  ty <- inferType Nothing val {- FIXME: This sometimes gives us a type w/ unknowns, but we don't have any other way to get at the type -}
+  if not (containsUnknowns ty)
+    then bindNames (M.singleton (Qualified (BySourcePos $ spanStart ss) ident) (ty, nameKind, Defined)) $ do
+      thisDecl <- declToCoreFn mn (A.ValueDecl sa ident nameKind [] [A.MkUnguarded (A.TypedValue False val ty)])
+      let seen' = seen ++ thisDecl
+      transformLetBindings mn _ss seen' rest ret
+    else  error
+            $ "The inferred type for let-bound identifier \n   '"
+              <> showIdent' ident
+              <> "'\ncontains unification variables:\n "
+              <> ppType 1000 ty
+              <> "\nPlease add a type signature for '" <> showIdent' ident <> "'"
 -- NOTE/TODO: This is super hack-ey. Ugh.
 transformLetBindings mn _ss seen (A.BindingGroupDeclaration ds : rest) ret = wrapTrace "transformLetBindings BINDINGGROUPDEC" $ do
   SplitBindingGroup untyped typed dict <- typeDictionaryForBindingGroup Nothing . NEL.toList $ fmap (\(i, _, v) -> (i, v)) ds
   if null untyped
     then do
-      let ds' =  flip map typed $ \((sann,iden),(expr,_,ty,_)) ->  A.ValueDecl sann iden Private [] [A.MkUnguarded (A.TypedValue False expr ty)]
+      let ds' =  flip map typed $ \((sann,iden),(expr,_,ty,_)) -> A.ValueDecl sann iden Private [] [A.MkUnguarded (A.TypedValue False expr ty)]
       bindNames dict $ do
         makeBindingGroupVisible
-        thisDecl <- concat <$> traverse (declToCoreFn mn)  ds'
+        thisDecl <- concat <$> traverse (declToCoreFn mn) ds'
         let seen' = seen ++ thisDecl
         transformLetBindings mn _ss seen' rest ret
     -- Because this has already been through the typechecker once, every value in the binding group should have an explicit type. I hope.
-    else error $ "untyped binding group element after initial typechecker pass: \n" <> LT.unpack (pShow untyped)
+    else error $ "untyped binding group element in mutually recursive LET binding group after initial typechecker pass: \n" <> LT.unpack (pShow untyped)
 transformLetBindings _ _ _ _ _ = error "Invalid argument to TransformLetBindings"
 
--- TODO: Make less convoluted
--- Problem: Doesn't give us kind information. Do we need it?
-generalizeUnknowns :: forall (m :: * -> *) (a :: *). M m => Type a -> m (Type a)
-generalizeUnknowns t = do
-  let unks = IS.toList $  unknowns t
-  t' <- foldM gogo t unks
-  pure . quantify $ t'
-  where
-    go :: T.Text -> Int -> Type a -> m (Type a)
-    go nm ti = \case
-      tu@(TUnknown ann i) ->
-        if i == ti
-          then pure $ TypeVar ann nm
-          else pure tu
-      other -> pure other
-
-    gogo :: Type a -> IS.Key -> m (Type a)
-    gogo acc i = lookupUnkName i >>= \case
-      Just nm -> everywhereOnTypesM (go nm i) acc
-      Nothing -> do
-        fresh <- runIdent <$> freshIdent'
-        everywhereOnTypesM (go fresh i) acc
-
 
 -- | Infer the types of variables brought into scope by a binder *without* instantiating polytypes to unknowns.
 -- TODO: Check whether unifyTypes needed

src/Language/PureScript/CoreFn/Desugar/Utils.hs

@@ -4,7 +4,8 @@
 module Language.PureScript.CoreFn.Desugar.Utils where
 
 import Prelude
-import Protolude (MonadError (..))
+import Prelude qualified as P
+import Protolude (MonadError (..), traverse_)
 
 import Data.Function (on)
 import Data.Tuple (swap)
@@ -24,7 +25,7 @@ import Language.PureScript.Types (SourceType, Type(..), Constraint (..), srcType
 import Language.PureScript.AST.Binders qualified as A
 import Language.PureScript.AST.Declarations qualified as A
 import Control.Monad.Supply.Class (MonadSupply)
-import Control.Monad.State.Strict (MonadState, gets)
+import Control.Monad.State.Strict (MonadState, gets, modify')
 import Control.Monad.Writer.Class ( MonadWriter )
 import Language.PureScript.TypeChecker.Types
     ( kindType,
@@ -41,7 +42,7 @@ import Language.PureScript.TypeChecker.Monad
     ( bindLocalVariables,
       getEnv,
       withScopedTypeVars,
-      CheckState(checkCurrentModule, checkEnv) )
+      CheckState(checkCurrentModule, checkEnv), debugNames )
 import Language.PureScript.Pretty.Values (renderValue)
 
 
@@ -63,9 +64,11 @@ traverseLit f = \case
 -- | When we call `exprToCoreFn` we sometimes know the type, and sometimes have to infer it. This just simplifies the process of getting the type we want (cuts down on duplicated code)
 inferType :: M m => Maybe SourceType -> A.Expr -> m SourceType
 inferType (Just t) _ = pure t
-inferType Nothing e = traceM ("**********HAD TO INFER TYPE FOR: " <> renderValue 100 e) >>
+inferType Nothing e = traceM ("**********HAD TO INFER TYPE FOR: (" <> renderValue 100 e <> ")") >>
   infer e >>= \case
-    TypedValue' _ _ t -> pure t
+    TypedValue' _ _ t -> do
+      traceM ("TYPE: " <> ppType 100 t)
+      pure t
 
 {- This function more-or-less contains our strategy for handling polytypes (quantified or constrained types). It returns a tuple T such that:
      - T[0] is the inner type, where all of the quantifiers and constraints have been removed. We just instantiate the quantified type variables to themselves (I guess?) - the previous
@@ -102,6 +105,42 @@ instantiatePolyType mn = \case
   other -> (other,id,id)
 
 
+traceNameTypes :: M m => m ()
+traceNameTypes  = do
+  nametypes <- getEnv >>= pure . debugNames
+  traverse_ traceM nametypes
+
+{- Since we operate on an AST where constraints have been desugared to dictionaries at the *expr* level,
+   using a typechecker context which contains ConstrainedTypes, looking up the type for a class method
+   will always give us a "wrong" type. Let's try fixing them in the context!
+
+-}
+desugarConstraintType' :: SourceType -> SourceType
+desugarConstraintType' = \case
+  ForAll a vis var mbk t mSkol ->
+    let t' = desugarConstraintType' t
+    in ForAll a vis var mbk t' mSkol
+  ConstrainedType _ Constraint{..} t ->
+    let inner = desugarConstraintType' t
+        dictTyName :: Qualified (ProperName 'TypeName) = dictTypeName . coerceProperName <$> constraintClass
+        dictTyCon = srcTypeConstructor dictTyName
+        dictTy = foldl srcTypeApp dictTyCon constraintArgs
+    in function dictTy inner
+  other -> other
+
+desugarConstraintType :: M m => Qualified Ident -> m ()
+desugarConstraintType i = do
+  env <- getEnv
+  let oldNameTypes = names env
+  case M.lookup i oldNameTypes of
+    Just (t,k,v) -> do
+      let newVal = (desugarConstraintType' t, k, v)
+          newNameTypes = M.insert i newVal oldNameTypes
+          newEnv = env {names = newNameTypes}
+      modify' $ \checkstate -> checkstate {checkEnv = newEnv}
+
+
+
 -- Gives much more readable output (with colors for brackets/parens!) than plain old `show`
 pTrace :: (Monad m, Show a) => a -> m ()
 pTrace = traceM . LT.unpack . pShow