Skip to content

Commit 284cefc

Browse files
purefunctorpurefunctor
authored
Defer monomorphization for data constructors (#4376)
1 parent d778505 commit 284cefc

5 files changed

Lines changed: 188 additions & 37 deletions

File tree

‎CHANGELOG.d/fix_polymorhic_constructors.md‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
* Defer monomorphization for data constructors
2+
3+
In `0.15.4` and earlier, the compiler monomorphizes type
4+
constructors early, yielding the following type:
5+
6+
```purs
7+
> :t Nothing
8+
forall (a1 :: Type). Maybe a1
9+
10+
> :t { a : Nothing }
11+
forall (a1 :: Type).
12+
{ a :: Maybe a1
13+
}
14+
```
15+
16+
With this change, the monomorphization introduced in
17+
[#835](https://github.com/purescript/purescript/pull/835) is
18+
deferred to only when it's needed, such as when constructors are
19+
used as values inside of records.
20+
21+
```purs
22+
> :t Nothing
23+
forall a. Maybe a
24+
25+
> :t { a : Nothing }
26+
forall (a1 :: Type).
27+
{ a :: Maybe a1
28+
}
29+
```
30+
31+
Also as a consequence, record updates should not throw
32+
`ConstrainedTypeUnified` in cases such as:
33+
34+
```purs
35+
v1 :: { a :: Maybe Unit }
36+
v1 = { a : Just Unit }
37+
38+
v2 :: { a :: Maybe Unit }
39+
v2 = let v3 = v1 { a = mempty } in v3
40+
```

‎src/Language/PureScript/TypeChecker/Types.hs‎

Lines changed: 97 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@ import Language.PureScript.Crash (internalError)
5050
import Language.PureScript.Environment
5151
import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), errorMessage, errorMessage', escalateWarningWhen, internalCompilerError, onErrorMessages, onTypesInErrorMessage, parU)
5252
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, freshIdent)
53-
import Language.PureScript.Traversals (sndM)
5453
import Language.PureScript.TypeChecker.Deriving (deriveInstance)
5554
import Language.PureScript.TypeChecker.Entailment (InstanceContext, newDictionaries, replaceTypeClassDictionaries)
5655
import Language.PureScript.TypeChecker.Kinds (checkConstraint, checkTypeKind, kindOf, kindOfWithScopedVars, unifyKinds', unknownsWithKinds)
@@ -369,38 +368,62 @@ infer' (Literal ss (ArrayLiteral vals)) = do
369368
return $ TypedValue' True (Literal ss (ArrayLiteral ts')) (srcTypeApp tyArray els)
370369
infer' (Literal ss (ObjectLiteral ps)) = do
371370
ensureNoDuplicateProperties ps
372-
-- We make a special case for Vars in record labels, since these are the
373-
-- only types of expressions for which 'infer' can return a polymorphic type.
374-
-- They need to be instantiated here.
375-
let shouldInstantiate :: Expr -> Bool
376-
shouldInstantiate Var{} = True
377-
shouldInstantiate (PositionedValue _ _ e) = shouldInstantiate e
378-
shouldInstantiate _ = False
379-
380-
inferProperty :: (PSString, Expr) -> m (PSString, (Expr, SourceType))
381-
inferProperty (name, val) = do
382-
TypedValue' _ val' ty <- infer val
383-
valAndType <- if shouldInstantiate val
384-
then instantiatePolyTypeWithUnknowns val' ty
385-
else pure (val', ty)
386-
pure (name, valAndType)
387-
388-
toRowListItem (lbl, (_, ty)) = srcRowListItem (Label lbl) ty
389-
390-
fields <- forM ps inferProperty
391-
let ty = srcTypeApp tyRecord $ rowFromList (map toRowListItem fields, srcKindApp srcREmpty kindType)
392-
return $ TypedValue' True (Literal ss (ObjectLiteral (map (fmap (uncurry (TypedValue True))) fields))) ty
393-
infer' (ObjectUpdate o ps) = do
371+
typedFields <- inferProperties ps
372+
let
373+
toRowListItem :: (PSString, (Expr, SourceType)) -> RowListItem SourceAnn
374+
toRowListItem (l, (_, t)) = srcRowListItem (Label l) t
375+
376+
recordType :: SourceType
377+
recordType = srcTypeApp tyRecord $ rowFromList (toRowListItem <$> typedFields, srcKindApp srcREmpty kindType)
378+
379+
typedProperties :: [(PSString, Expr)]
380+
typedProperties = fmap (fmap (uncurry (TypedValue True))) typedFields
381+
pure $ TypedValue' True (Literal ss (ObjectLiteral typedProperties)) recordType
382+
infer' (ObjectUpdate ob ps) = do
394383
ensureNoDuplicateProperties ps
395-
row <- freshTypeWithKind (kindRow kindType)
396-
typedVals <- zipWith (\(name, _) t -> (name, t)) ps <$> traverse (infer . snd) ps
397-
let toRowListItem = uncurry srcRowListItem
398-
let newTys = map (\(name, TypedValue' _ _ ty) -> (Label name, ty)) typedVals
399-
oldTys <- zip (map (Label . fst) ps) <$> replicateM (length ps) (freshTypeWithKind kindType)
400-
let oldTy = srcTypeApp tyRecord $ rowFromList (toRowListItem <$> oldTys, row)
401-
o' <- TypedValue True <$> (tvToExpr <$> check o oldTy) <*> pure oldTy
402-
let newVals = map (fmap tvToExpr) typedVals
403-
return $ TypedValue' True (ObjectUpdate o' newVals) $ srcTypeApp tyRecord $ rowFromList (toRowListItem <$> newTys, row)
384+
-- This "tail" holds all other fields not being updated.
385+
rowType <- freshTypeWithKind (kindRow kindType)
386+
let updateLabels = Label . fst <$> ps
387+
-- Generate unification variables for each field in ps.
388+
--
389+
-- Given:
390+
--
391+
-- ob { a = 0, b = 0 }
392+
--
393+
-- Then:
394+
--
395+
-- obTypes = [(a, ?0), (b, ?1)]
396+
obTypes <- zip updateLabels <$> replicateM (length updateLabels) (freshTypeWithKind kindType)
397+
let obItems :: [RowListItem SourceAnn]
398+
obItems = uncurry srcRowListItem <$> obTypes
399+
-- Create a record type that contains the unification variables.
400+
--
401+
-- obRecordType = Record ( a :: ?0, b :: ?1 | rowType )
402+
obRecordType :: SourceType
403+
obRecordType = srcTypeApp tyRecord $ rowFromList (obItems, rowType)
404+
-- Check ob against obRecordType.
405+
--
406+
-- Given:
407+
--
408+
-- ob : { a :: Int, b :: Int }
409+
--
410+
-- Then:
411+
--
412+
-- ?0 ~ Int
413+
-- ?1 ~ Int
414+
-- ob' : { a :: ?0, b :: ?1 }
415+
ob' <- TypedValue True <$> (tvToExpr <$> check ob obRecordType) <*> pure obRecordType
416+
-- Infer the types of the values used for the record update.
417+
typedFields <- inferProperties ps
418+
let newItems :: [RowListItem SourceAnn]
419+
newItems = (\(l, (_, t)) -> srcRowListItem (Label l) t) <$> typedFields
420+
421+
ps' :: [(PSString, Expr)]
422+
ps' = (\(l, (e, t)) -> (l, TypedValue True e t)) <$> typedFields
423+
424+
newRecordType :: SourceType
425+
newRecordType = srcTypeApp tyRecord $ rowFromList (newItems, rowType)
426+
pure $ TypedValue' True (ObjectUpdate ob' ps') newRecordType
404427
infer' (Accessor prop val) = withErrorMessageHint (ErrorCheckingAccessor val prop) $ do
405428
field <- freshTypeWithKind kindType
406429
rest <- freshTypeWithKind (kindRow kindType)
@@ -431,8 +454,7 @@ infer' v@(Constructor _ c) = do
431454
env <- getEnv
432455
case M.lookup c (dataConstructors env) of
433456
Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
434-
Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
435-
return $ TypedValue' True v' ty'
457+
Just (_, _, ty, _) -> TypedValue' True v <$> (introduceSkolemScope <=< replaceAllTypeSynonyms $ ty)
436458
infer' (Case vals binders) = do
437459
(vals', ts) <- instantiateForBinders vals binders
438460
ret <- freshTypeWithKind kindType
@@ -474,6 +496,44 @@ infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
474496
return $ TypedValue' t (PositionedValue pos c v) ty
475497
infer' v = internalError $ "Invalid argument to infer: " ++ show v
476498

499+
-- |
500+
-- Infer the types of named record fields.
501+
inferProperties
502+
:: ( MonadSupply m
503+
, MonadState CheckState m
504+
, MonadError MultipleErrors m
505+
, MonadWriter MultipleErrors m
506+
)
507+
=> [(PSString, Expr)]
508+
-> m [(PSString, (Expr, SourceType))]
509+
inferProperties = traverse (traverse inferWithinRecord)
510+
511+
-- |
512+
-- Infer the type of a value when used as a record field.
513+
inferWithinRecord
514+
:: ( MonadSupply m
515+
, MonadState CheckState m
516+
, MonadError MultipleErrors m
517+
, MonadWriter MultipleErrors m
518+
)
519+
=> Expr
520+
-> m (Expr, SourceType)
521+
inferWithinRecord e = do
522+
TypedValue' _ v t <- infer e
523+
if propertyShouldInstantiate e
524+
then instantiatePolyTypeWithUnknowns v t
525+
else pure (v, t)
526+
527+
-- |
528+
-- Determines if a value's type needs to be monomorphized when
529+
-- used inside of a record.
530+
propertyShouldInstantiate :: Expr -> Bool
531+
propertyShouldInstantiate = \case
532+
Var{} -> True
533+
Constructor{} -> True
534+
PositionedValue _ _ e -> propertyShouldInstantiate e
535+
_ -> False
536+
477537
inferLetBinding
478538
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
479539
=> [Declaration]
@@ -795,7 +855,7 @@ check' v@(Constructor _ c) ty = do
795855
Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
796856
Just (_, _, ty1, _) -> do
797857
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
798-
ty' <- introduceSkolemScope ty
858+
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
799859
elaborate <- subsumes repl ty'
800860
return $ TypedValue' True (elaborate v) ty'
801861
check' (Let w ds val) ty = do
@@ -841,11 +901,11 @@ checkProperties expr ps row lax = convert <$> go ps (toRowPair <$> ts') r' where
841901
go ((p,v):ps') ts r =
842902
case lookup (Label p) ts of
843903
Nothing -> do
844-
v'@(TypedValue' _ _ ty) <- infer v
904+
(v', ty) <- inferWithinRecord v
845905
rest <- freshTypeWithKind (kindRow kindType)
846906
unifyTypes r (srcRCons (Label p) ty rest)
847907
ps'' <- go ps' ts rest
848-
return $ (p, v') : ps''
908+
return $ (p, TypedValue' True v' ty) : ps''
849909
Just ty -> do
850910
v' <- check v ty
851911
ps'' <- go ps' (delete (Label p, ty) ts) r

‎tests/purs/passing/4376.purs‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
module Main where
2+
3+
import Prelude
4+
import Prim.Row (class Union)
5+
6+
import Data.Maybe (Maybe(..))
7+
import Data.Monoid (mempty)
8+
import Effect.Console (log)
9+
import Type.Proxy (Proxy(..))
10+
11+
-- Make sure that record updates get monomorphized.
12+
asNothing :: forall a. { a :: Maybe a } -> { a :: Maybe a }
13+
asNothing = _ { a = Nothing }
14+
15+
union :: forall a b c. Union a b c => Record a -> Record b -> Proxy c
16+
union _ _ = Proxy
17+
18+
-- This fails to solve if neither is monomorphized.
19+
shouldSolve :: forall a b. Proxy ( a :: Maybe a, b :: Maybe b )
20+
shouldSolve = { a: Nothing } `union` { b: Nothing }
21+
22+
-- Removes ConstrainedTypeUnified
23+
v1 :: { a :: Maybe Unit }
24+
v1 = { a : Just unit }
25+
26+
v2 :: { a :: Maybe Unit }
27+
v2 = let v3 = v1 { a = mempty } in v3
28+
29+
main = log "Done"

‎tests/purs/warning/4376.out‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
Warning found:
2+
in module Main
3+
at tests/purs/warning/4376.purs:6:1 - 6:16 (line 6, column 1 - line 6, column 16)
4+
5+
No type declaration was provided for the top-level declaration of value.
6+
It is good practice to provide type declarations as a form of documentation.
7+
The inferred type of value was:
8+
 
9+
 forall a. Maybe a
10+
 
11+
12+
in value declaration value
13+
14+
See https://github.com/purescript/documentation/blob/master/errors/MissingTypeDeclaration.md for more information,
15+
or to contribute content related to this warning.
16+

‎tests/purs/warning/4376.purs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
-- @shouldWarnWith MissingTypeDeclaration
2+
module Main where
3+
4+
data Maybe a = Just a | Nothing
5+
6+
value = Nothing

0 commit comments

Comments
 (0)