Defer monomorphization for data constructors (#4376)

purefunctor · web-flow · commit 284cefc60f75 · 2023-04-22T12:59:08.000+08:00
diff --git a/CHANGELOG.d/fix_polymorhic_constructors.md b/CHANGELOG.d/fix_polymorhic_constructors.md
@@ -0,0 +1,40 @@
+* Defer monomorphization for data constructors
+
+  In `0.15.4` and earlier, the compiler monomorphizes type
+  constructors early, yielding the following type:
+
+  ```purs
+  > :t Nothing
+  forall (a1 :: Type). Maybe a1
+
+  > :t { a : Nothing }
+  forall (a1 :: Type).
+    { a :: Maybe a1
+    }
+  ```
+
+  With this change, the monomorphization introduced in
+  [#835](https://github.com/purescript/purescript/pull/835) is
+  deferred to only when it's needed, such as when constructors are
+  used as values inside of records.
+
+  ```purs
+  > :t Nothing
+  forall a. Maybe a
+
+  > :t { a : Nothing }
+  forall (a1 :: Type).
+    { a :: Maybe a1
+    }
+  ```
+
+  Also as a consequence, record updates should not throw
+  `ConstrainedTypeUnified` in cases such as:
+
+  ```purs
+  v1 :: { a :: Maybe Unit }
+  v1 = { a : Just Unit }
+
+  v2 :: { a :: Maybe Unit }
+  v2 = let v3 = v1 { a = mempty } in v3
+  ```
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
@@ -50,7 +50,6 @@ import Language.PureScript.Crash (internalError)
 import Language.PureScript.Environment
 import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), errorMessage, errorMessage', escalateWarningWhen, internalCompilerError, onErrorMessages, onTypesInErrorMessage, parU)
 import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, freshIdent)
-import Language.PureScript.Traversals (sndM)
 import Language.PureScript.TypeChecker.Deriving (deriveInstance)
 import Language.PureScript.TypeChecker.Entailment (InstanceContext, newDictionaries, replaceTypeClassDictionaries)
 import Language.PureScript.TypeChecker.Kinds (checkConstraint, checkTypeKind, kindOf, kindOfWithScopedVars, unifyKinds', unknownsWithKinds)
@@ -369,38 +368,62 @@ infer' (Literal ss (ArrayLiteral vals)) = do
   return $ TypedValue' True (Literal ss (ArrayLiteral ts')) (srcTypeApp tyArray els)
 infer' (Literal ss (ObjectLiteral ps)) = do
   ensureNoDuplicateProperties ps
-  -- We make a special case for Vars in record labels, since these are the
-  -- only types of expressions for which 'infer' can return a polymorphic type.
-  -- They need to be instantiated here.
-  let shouldInstantiate :: Expr -> Bool
-      shouldInstantiate Var{} = True
-      shouldInstantiate (PositionedValue _ _ e) = shouldInstantiate e
-      shouldInstantiate _ = False
-
-      inferProperty :: (PSString, Expr) -> m (PSString, (Expr, SourceType))
-      inferProperty (name, val) = do
-        TypedValue' _ val' ty <- infer val
-        valAndType <- if shouldInstantiate val
-                        then instantiatePolyTypeWithUnknowns val' ty
-                        else pure (val', ty)
-        pure (name, valAndType)
-
-      toRowListItem (lbl, (_, ty)) = srcRowListItem (Label lbl) ty
-
-  fields <- forM ps inferProperty
-  let ty = srcTypeApp tyRecord $ rowFromList (map toRowListItem fields, srcKindApp srcREmpty kindType)
-  return $ TypedValue' True (Literal ss (ObjectLiteral (map (fmap (uncurry (TypedValue True))) fields))) ty
-infer' (ObjectUpdate o ps) = do
+  typedFields <- inferProperties ps
+  let
+    toRowListItem :: (PSString, (Expr, SourceType)) -> RowListItem SourceAnn
+    toRowListItem (l, (_, t)) = srcRowListItem (Label l) t
+
+    recordType :: SourceType
+    recordType = srcTypeApp tyRecord $ rowFromList (toRowListItem <$> typedFields, srcKindApp srcREmpty kindType)
+
+    typedProperties :: [(PSString, Expr)]
+    typedProperties = fmap (fmap (uncurry (TypedValue True))) typedFields
+  pure $ TypedValue' True (Literal ss (ObjectLiteral typedProperties)) recordType
+infer' (ObjectUpdate ob ps) = do
   ensureNoDuplicateProperties ps
-  row <- freshTypeWithKind (kindRow kindType)
-  typedVals <- zipWith (\(name, _) t -> (name, t)) ps <$> traverse (infer . snd) ps
-  let toRowListItem = uncurry srcRowListItem
-  let newTys = map (\(name, TypedValue' _ _ ty) -> (Label name, ty)) typedVals
-  oldTys <- zip (map (Label . fst) ps) <$> replicateM (length ps) (freshTypeWithKind kindType)
-  let oldTy = srcTypeApp tyRecord $ rowFromList (toRowListItem <$> oldTys, row)
-  o' <- TypedValue True <$> (tvToExpr <$> check o oldTy) <*> pure oldTy
-  let newVals = map (fmap tvToExpr) typedVals
-  return $ TypedValue' True (ObjectUpdate o' newVals) $ srcTypeApp tyRecord $ rowFromList (toRowListItem <$> newTys, row)
+  -- This "tail" holds all other fields not being updated.
+  rowType <- freshTypeWithKind (kindRow kindType)
+  let updateLabels = Label . fst <$> ps
+  -- Generate unification variables for each field in ps.
+  --
+  -- Given:
+  --
+  -- ob { a = 0, b = 0 }
+  --
+  -- Then:
+  --
+  -- obTypes = [(a, ?0), (b, ?1)]
+  obTypes <- zip updateLabels <$> replicateM (length updateLabels) (freshTypeWithKind kindType)
+  let obItems :: [RowListItem SourceAnn]
+      obItems = uncurry srcRowListItem <$> obTypes
+      -- Create a record type that contains the unification variables.
+      --
+      -- obRecordType = Record ( a :: ?0, b :: ?1 | rowType )
+      obRecordType :: SourceType
+      obRecordType = srcTypeApp tyRecord $ rowFromList (obItems, rowType)
+  -- Check ob against obRecordType.
+  --
+  -- Given:
+  --
+  -- ob : { a :: Int, b :: Int }
+  --
+  -- Then:
+  --
+  -- ?0  ~  Int
+  -- ?1  ~  Int
+  -- ob' : { a :: ?0, b :: ?1 }
+  ob' <- TypedValue True <$> (tvToExpr <$> check ob obRecordType) <*> pure obRecordType
+  -- Infer the types of the values used for the record update.
+  typedFields <- inferProperties ps
+  let newItems :: [RowListItem SourceAnn]
+      newItems = (\(l, (_, t)) -> srcRowListItem (Label l) t) <$> typedFields
+
+      ps' :: [(PSString, Expr)]
+      ps' = (\(l, (e, t)) -> (l, TypedValue True e t)) <$> typedFields
+
+      newRecordType :: SourceType
+      newRecordType = srcTypeApp tyRecord $ rowFromList (newItems, rowType)
+  pure $ TypedValue' True (ObjectUpdate ob' ps') newRecordType
 infer' (Accessor prop val) = withErrorMessageHint (ErrorCheckingAccessor val prop) $ do
   field <- freshTypeWithKind kindType
   rest <- freshTypeWithKind (kindRow kindType)
@@ -431,8 +454,7 @@ infer' v@(Constructor _ c) = do
   env <- getEnv
   case M.lookup c (dataConstructors env) of
     Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
-    Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
-                             return $ TypedValue' True v' ty'
+    Just (_, _, ty, _) -> TypedValue' True v <$> (introduceSkolemScope <=< replaceAllTypeSynonyms $ ty)
 infer' (Case vals binders) = do
   (vals', ts) <- instantiateForBinders vals binders
   ret <- freshTypeWithKind kindType
@@ -474,6 +496,44 @@ infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
   return $ TypedValue' t (PositionedValue pos c v) ty
 infer' v = internalError $ "Invalid argument to infer: " ++ show v
 
+-- |
+-- Infer the types of named record fields.
+inferProperties
+  :: ( MonadSupply m
+     , MonadState CheckState m
+     , MonadError MultipleErrors m
+     , MonadWriter MultipleErrors m
+     )
+  => [(PSString, Expr)]
+  -> m [(PSString, (Expr, SourceType))]
+inferProperties = traverse (traverse inferWithinRecord)
+
+-- |
+-- Infer the type of a value when used as a record field.
+inferWithinRecord
+  :: ( MonadSupply m
+     , MonadState CheckState m
+     , MonadError MultipleErrors m
+     , MonadWriter MultipleErrors m
+     )
+  => Expr
+  -> m (Expr, SourceType)
+inferWithinRecord e = do
+  TypedValue' _ v t <- infer e
+  if propertyShouldInstantiate e
+    then instantiatePolyTypeWithUnknowns v t
+    else pure (v, t)
+
+-- |
+-- Determines if a value's type needs to be monomorphized when
+-- used inside of a record.
+propertyShouldInstantiate :: Expr -> Bool
+propertyShouldInstantiate = \case
+  Var{} -> True
+  Constructor{} -> True
+  PositionedValue _ _ e -> propertyShouldInstantiate e
+  _ -> False
+
 inferLetBinding
   :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
   => [Declaration]
@@ -795,7 +855,7 @@ check' v@(Constructor _ c) ty = do
     Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
     Just (_, _, ty1, _) -> do
       repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
-      ty' <- introduceSkolemScope ty
+      ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
       elaborate <- subsumes repl ty'
       return $ TypedValue' True (elaborate v) ty'
 check' (Let w ds val) ty = do
@@ -841,11 +901,11 @@ checkProperties expr ps row lax = convert <$> go ps (toRowPair <$> ts') r' where
   go ((p,v):ps') ts r =
     case lookup (Label p) ts of
       Nothing -> do
-        v'@(TypedValue' _ _ ty) <- infer v
+        (v', ty) <- inferWithinRecord v
         rest <- freshTypeWithKind (kindRow kindType)
         unifyTypes r (srcRCons (Label p) ty rest)
         ps'' <- go ps' ts rest
-        return $ (p, v') : ps''
+        return $ (p, TypedValue' True v' ty) : ps''
       Just ty -> do
         v' <- check v ty
         ps'' <- go ps' (delete (Label p, ty) ts) r
diff --git a/tests/purs/passing/4376.purs b/tests/purs/passing/4376.purs
@@ -0,0 +1,29 @@
+module Main where
+
+import Prelude
+import Prim.Row (class Union)
+
+import Data.Maybe (Maybe(..))
+import Data.Monoid (mempty)
+import Effect.Console (log)
+import Type.Proxy (Proxy(..))
+
+-- Make sure that record updates get monomorphized.
+asNothing :: forall a. { a :: Maybe a } -> { a :: Maybe a }
+asNothing = _ { a = Nothing }
+
+union :: forall a b c. Union a b c => Record a -> Record b -> Proxy c
+union _ _ = Proxy
+
+-- This fails to solve if neither is monomorphized.
+shouldSolve :: forall a b. Proxy ( a :: Maybe a, b :: Maybe b )
+shouldSolve = { a: Nothing } `union` { b: Nothing }
+
+-- Removes ConstrainedTypeUnified
+v1 :: { a :: Maybe Unit }
+v1 = { a : Just unit }
+
+v2 :: { a :: Maybe Unit }
+v2 = let v3 = v1 { a = mempty } in v3
+
+main = log "Done"
diff --git a/tests/purs/warning/4376.out b/tests/purs/warning/4376.out
@@ -0,0 +1,16 @@
+Warning found:
+in module [33mMain[0m
+at tests/purs/warning/4376.purs:6:1 - 6:16 (line 6, column 1 - line 6, column 16)
+
+  No type declaration was provided for the top-level declaration of [33mvalue[0m.
+  It is good practice to provide type declarations as a form of documentation.
+  The inferred type of [33mvalue[0m was:
+  [33m                   [0m
+  [33m  forall a. Maybe a[0m
+  [33m                   [0m
+
+in value declaration [33mvalue[0m
+
+See https://github.com/purescript/documentation/blob/master/errors/MissingTypeDeclaration.md for more information,
+or to contribute content related to this warning.
+
diff --git a/tests/purs/warning/4376.purs b/tests/purs/warning/4376.purs
@@ -0,0 +1,6 @@
+-- @shouldWarnWith MissingTypeDeclaration
+module Main where
+
+data Maybe a = Just a | Nothing
+
+value = Nothing

-Original file line number
+Diff line change
@@ @@ -0,0 +1,16 @@ @@
 +Warning found:
 +in module [33mMain[0m
 +at tests/purs/warning/4376.purs:6:1 - 6:16 (line 6, column 1 - line 6, column 16)
++
 +  No type declaration was provided for the top-level declaration of [33mvalue[0m.
 +  It is good practice to provide type declarations as a form of documentation.
 +  The inferred type of [33mvalue[0m was:
 +  [33m                   [0m
 +  [33m  forall a. Maybe a[0m
 +  [33m                   [0m
++
 +in value declaration [33mvalue[0m
++
 +See https://github.com/purescript/documentation/blob/master/errors/MissingTypeDeclaration.md for more information,
 +or to contribute content related to this warning.
++