Guard/case desugaring w/ correct types

src/Language/PureScript/CoreFn/Desugar.hs

@@ -391,16 +391,25 @@ exprToCoreFn mn ss mTy app@(A.App fun arg)
 -- Dunno what to do here. Haven't encountered an Unused so far, will need to see one to figure out how to handle them
 exprToCoreFn _ _  _ (A.Unused _) = -- ????? need to figure out what this _is_
   error "Don't know what to do w/ exprToCoreFn A.Unused"
--- Variables should *always* be bound & typed in the Environment before we encounter them.
+
+exprToCoreFn _ _ (Just ty) (A.Var ss ident@(Qualified _ (GenIdent _ _))) = wrapTrace ("exprToCoreFn VAR (gen) " <> show ident) $
+  gets checkEnv >>= \env ->
+     pure $ Var (ss, [], getValueMeta env ident) (purusTy ty) ident
+-- Non-generated Variables should *always* be bound & typed in the Environment before we encounter them.
 -- NOTE: Not sure if we should ignore a type passed in? Generally we shouldn't *pass* types here, but bind variables
 exprToCoreFn _ _ _ (A.Var ss ident) = wrapTrace ("exprToCoreFn VAR " <> show ident) $
   gets checkEnv >>= \env -> case lookupValue env ident of
     Just (ty,_,_) -> pure $ Var (ss, [], getValueMeta env ident) (purusTy ty) ident
     Nothing -> lookupDictType ident >>= \case
       Just ty -> pure $  Var (ss, [], getValueMeta env ident) (purusTy ty) ident
-      Nothing -> do
-        traceM $ "No known type for identifier " <> show ident
-        error "boom"
+      Nothing -> internalError $ "No known type for identifier " <> show ident
+
+exprToCoreFn _ _ mty expr@(A.Var ss ident) = internalError
+  $ "Internal compiler error (exprToCoreFn var fail): Cannot synthesize type for var "
+    <> show expr
+    <> "\nSupplied type: "
+    <> show (ppType 100 <$> mty)
+
 -- If-Then-Else Turns into a case expression
 exprToCoreFn mn ss (Just resT) (A.IfThenElse cond th el) = wrapTrace "exprToCoreFn IFTE" $ do
   condE <- exprToCoreFn mn ss (Just tyBoolean) cond
@@ -421,13 +430,44 @@ exprToCoreFn _ _  (Just ctorTy) (A.Constructor ss name) = wrapTrace ("exprToCore
 exprToCoreFn _ _ Nothing ctor@(A.Constructor _ _) =
   internalError $ "Error while desugaring Constructor expression. No type provided for:\n" <> renderValue 100 ctor
 
--- Case expressions
+{- Case Expressions
+
+   For ordinary case expressions (i.e. those not generated by the compiler during guard desugaring),
+   the type can be determined by the type of a top-level declaration or
+   explicit type annotation (which may be either supplied by the user or inferred by the
+   PS typechecker) and therefore should be passed explicitly.
+
+   For compiler-generated case expressions (specifically: those generated during case/guard desugaring -
+   some get generated during typeclass desugaring but we have special machinery to ensure that
+   those types can be synthesized), we cannot be sure that the whole case expression has an explicit
+   type annotation, so we try to deduce the type from the types of the alternative branches.
+
+   NOTE: This is kind of a hack to let us reuse (rather than rewrite) the existing case
+         desugaring machinery. In order to correctly type the generated `let` bindings
+         (see Language.PureScript.Sugar.CaseDeclarations), we must manually construct a polymorphic
+         type that the PS typechecker cannot infer or deduce. We cannot construct such a type without
+         the initial PS typechecker pass. We could write two nearly-identical versions of the
+         case desugaring machinery and try to run the typechecker twice, but that adds a lot of
+         complexity (machinery is complicated) and would not be good for performance (typechecking
+         and inference have bad complexity).
+
+-}
 exprToCoreFn mn ss (Just caseTy) astCase@(A.Case vs alts) = wrapTrace "exprToCoreFn CASE" $ do
   traceM $ "CASE:\n" <> renderValue 100 astCase
   traceM $ "CASE TY:\n" <> show (ppType 100 caseTy)
   (vs',ts) <- unzip <$> traverse (exprToCoreFn mn ss Nothing >=> (\ e -> pure (e, exprType e))) vs -- extract type information for the *scrutinees*
   alts' <- traverse (altToCoreFn mn ss caseTy ts) alts -- see explanation in altToCoreFn. We pass in the types of the scrutinee(s)
   pure $ Case (ssA ss) (purusTy caseTy) vs' alts'
+exprToCoreFn mn ss Nothing  astCase@(A.Case vs alts@(alt:_)) = wrapTrace "exprToCoreFn CASE (no type)" $ do
+  case alt of
+    A.CaseAlternative _ (A.GuardedExpr _ body1:_) -> do
+      caseTy <- exprType <$> exprToCoreFn mn ss Nothing body1
+      traceM $ "CASE:\n" <> renderValue 100 astCase
+      traceM $ "CASE TY:\n" <> show (ppType 100 caseTy)
+      (vs',ts) <- unzip <$> traverse (exprToCoreFn mn ss Nothing >=> (\ e -> pure (e, exprType e))) vs -- extract type information for the *scrutinees*
+      alts' <- traverse (altToCoreFn mn ss caseTy ts) alts -- see explanation in altToCoreFn. We pass in the types of the scrutinee(s)
+      pure $ Case (ssA ss) (purusTy caseTy) vs' alts'
+    _ -> internalError $ "Error while desugaring Case expression. Could not synthesize type of: " <> renderValue 100 astCase
 exprToCoreFn _ _ Nothing astCase@(A.Case _ _) =
   internalError $ "Error while desugaring Case expression. No type provided for:\n" <> renderValue 100 astCase
 

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

@@ -124,8 +124,9 @@ prettyValue (ObjectUpdate _ _ty o _copyFields ps)  = do
 prettyValue app@(App _  t1 t2)  = case analyzeApp app of
   Just (fun,args) -> do
     atom <- fmtSep =<< traverse prettyValueAtom (fun:args)
-    ty   <- prettyType $ appType t1 t2
-    pure . group . align $ parens (atom <:> ty)
+    pure . group . align $ atom
+    -- ty   <- prettyType $ appType t1 t2
+    -- pure . group . align $ parens (atom <:> ty)
     {- TODO: change back
     ask >>= \case
     OneLine -> pure . group . align . hsep .  map (asOneLine prettyValueAtom) $ (fun:args)
@@ -170,8 +171,8 @@ prettyValueAtom (Var _ ty ident)  =  prettyType ty >>= \ty' ->
   pure . parens $ pretty  (showIdent (disqualify ident)) <:> ty'
 prettyValueAtom expr = do -- TODO change this back (need more anns for testing)
   v <- prettyValue expr
-  t <- prettyType (exprType expr)
-  pure $ parens (v <:> t)
+  -- t <- prettyType (exprType expr)
+  pure $ parens v -- <:> t)
 
 prettyLiteralValue :: Literal (Expr a) -> Printer ann
 prettyLiteralValue (NumericLiteral n) = ignoreFmt $ pretty $ either show show n

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

@@ -72,7 +72,7 @@ prettyType t  =  group <$> case t of
 
   ConstrainedType _ _ _ -> error "TODO: ConstrainedType (shouldn't ever appear in Purus CoreFn)"
 
-  Skolem _ _ _ _ _ -> error "TODO: Skolem (shouldn't ever appear in Purus CoreFn)"
+  Skolem _ var _ i _ -> pure $ pretty var <> "#" <> pretty i
 
   REmpty _ -> pure "{}"
 
@@ -142,7 +142,7 @@ prettyType t  =  group <$> case t of
          REmpty _ -> pure $ Right []
          KindApp _ REmpty{} _  -> pure $ Right [] -- REmpty is sometimes wrapped in a kind app
          TypeVar _ txt -> pure $ Left ([],pretty txt)
-         other -> error $ "Malformed row fields: \n" <> prettyTypeStr other
+         other -> Right . pure <$> prettyType other  --  error $ "Malformed row fields: \n" <> prettyTypeStr other
 
 
 -- TODO For debugging, remove later

src/Language/PureScript/Sugar/CaseDeclarations.hs

@@ -17,15 +17,17 @@ import Data.Maybe (catMaybes, mapMaybe)
 
 import Control.Monad ((<=<), forM, replicateM, join, unless)
 import Control.Monad.Error.Class (MonadError(..))
-import Control.Monad.Supply.Class (MonadSupply)
+import Control.Monad.Supply.Class (MonadSupply, freshName)
 
 import Language.PureScript.AST
 import Language.PureScript.Crash (internalError)
-import Language.PureScript.Environment (NameKind(..))
+import Language.PureScript.Environment (NameKind(..), function)
 import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors(..), SimpleErrorMessage(..), addHint, errorMessage', parU, rethrow, withPosition)
-import Language.PureScript.Names (pattern ByNullSourcePos, Ident, Qualified(..), freshIdent')
+import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), Qualified(..), freshIdent')
 import Language.PureScript.TypeChecker.Monad (guardWith)
 
+import Debug.Trace
+import Language.PureScript.Types (SourceType, Type (TypeVar), quantify)
 -- |
 -- Replace all top-level binders in a module with case expressions.
 --
@@ -64,8 +66,9 @@ desugarGuardedExprs ss (Case scrut alternatives)
     -- we may evaluate the scrutinee more than once when a guard occurs.
     -- We bind the scrutinee to Vars here to mitigate this case.
     (scrut', scrut_decls) <- unzip <$> forM scrut (\e -> do
+      let mkTyped ex = TypedValue False ex (unsafeExprType e)
       scrut_id <- freshIdent'
-      pure ( Var ss (Qualified ByNullSourcePos scrut_id)
+      pure ( mkTyped $ Var ss (Qualified ByNullSourcePos scrut_id)
            , ValueDecl (ss, []) scrut_id Private [] [MkUnguarded e]
            )
       )
@@ -79,6 +82,8 @@ desugarGuardedExprs ss (Case scrut alternatives)
     isTrivialExpr (TypedValue _ e _) = isTrivialExpr e
     isTrivialExpr _ = False
 
+
+
 desugarGuardedExprs ss (Case scrut alternatives) =
   let
     -- Alternatives which do not have guards are
@@ -177,6 +182,10 @@ desugarGuardedExprs ss (Case scrut alternatives) =
           alt_fail' n | all isIrrefutable vb = []
                       | otherwise = alt_fail n
 
+          eTy = unsafeExprType e
+
+          mkType ex = TypedValue False ex eTy
+
 
           -- we are here:
           --
@@ -187,7 +196,7 @@ desugarGuardedExprs ss (Case scrut alternatives) =
           --        in case scrut of -- we are here
           --            ...
           --
-        in Case scrut
+        in mkType $ Case scrut
             (CaseAlternative vb [MkUnguarded (desugarGuard gs e alt_fail)]
               : alt_fail' (length scrut))
 
@@ -227,16 +236,23 @@ desugarGuardedExprs ss (Case scrut alternatives) =
         rem_case_id   <- freshIdent'
         unused_binder <- freshIdent'
 
+        freshTyVar <- freshName
+
         let
+          remTy = quantify $ function (TypeVar (ss,[]) freshTyVar) (unsafeExprType desugared)
+          mkType e = TypedValue False e remTy
+
           goto_rem_case :: Expr
-          goto_rem_case = Var ss (Qualified ByNullSourcePos rem_case_id)
+          goto_rem_case = mkType (Var ss (Qualified ByNullSourcePos rem_case_id))
             `App` Literal ss (BooleanLiteral True)
           alt_fail :: Int -> [CaseAlternative]
           alt_fail n = [CaseAlternative (replicate n NullBinder) [MkUnguarded goto_rem_case]]
 
+
+
         pure $ Let FromLet [
           ValueDecl (ss, []) rem_case_id Private []
-            [MkUnguarded (Abs (VarBinder ss unused_binder) desugared)]
+            [MkUnguarded $ mkType (Abs (VarBinder ss unused_binder ) desugared)]
           ] (mk_body alt_fail)
 
       | otherwise
@@ -420,3 +436,7 @@ makeCaseDeclaration ss ident alternatives = do
     | a == b = Just a
     | otherwise = Nothing
   resolveName _ _ = Nothing
+
+unsafeExprType :: Expr -> SourceType
+unsafeExprType (TypedValue _ _ t) = t
+unsafeExprType other = error $ "INTERNAL ERROR: Expected a TypedValue during case desugaring but got: " <> show other

tests/purus/passing/4310/output/Lib/index.cfn.pretty

@@ -22,10 +22,8 @@ Test$Dict = \(x: { runTest :: a -> String }) -> (x: { runTest :: a -> String })
 
 testInt :: Test$Dict Int
 testInt = 
-  ((Test$Dict: {   runTest :: Int -> String } -> Test$Dict Int)
-  ({ runTest: \(v: Int) -> ("4": String) }: {
-                                              runTest :: Int -> String
-                                            }): Test$Dict Int)
+  (Test$Dict: {   runTest :: Int -> String } -> Test$Dict Int)
+  ({ runTest: \(v: Int) -> ("4": String) }: { runTest :: Int -> String })
 
 runTest :: forall (@a :: Type). Test$Dict a -> a -> String
 runTest = 
@@ -40,17 +38,17 @@ test/\ :: forall (a :: Type) (b :: Type). Test$Dict a -> Test$Dict b -> Test$Dic
 test/\ = 
   \(dictTest: Test$Dict a) -> 
     \(dictTest1: Test$Dict b) -> 
-      ((Test$Dict: {   runTest :: (Tuple a b) -> String } ->
+      (Test$Dict: {   runTest :: (Tuple a b) -> String } ->
       Test$Dict (Tuple a b))
       ({
          runTest: \(v: (Tuple a b)) -> 
            case (v: (Tuple a b)) of 
               Tuple a b -> 
-                ((mappend: String -> String -> String)
-                (((runTest: forall (@a :: Type). Test$Dict a -> a -> String)
+                (mappend: String -> String -> String)
+                ((runTest: forall (@a :: Type). Test$Dict a -> a -> String)
                  (dictTest: Test$Dict a)
-                 (a: a): String): String)
-                (((runTest: forall (@a :: Type). Test$Dict a -> a -> String)
+                 (a: a))
+                ((runTest: forall (@a :: Type). Test$Dict a -> a -> String)
                  (dictTest1: Test$Dict b)
-                 (b: b): String): String): String)
-       }: { runTest :: (Tuple a b) -> String }): Test$Dict (Tuple a b))
+                 (b: b))
+       }: { runTest :: (Tuple a b) -> String })