Skip to content

Commit 6583706

Browse files
purefunctorpurefunctor
committed
Defer monomorphization for data constructors
1 parent 0b5a87e commit 6583706

5 files changed

Lines changed: 166 additions & 37 deletions

File tree

‎CHANGELOG.d/fix_polymorhic_constructors.md‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
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+
```

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

Lines changed: 93 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@ import Language.PureScript.Crash
5050
import Language.PureScript.Environment
5151
import Language.PureScript.Errors
5252
import Language.PureScript.Names
53-
import Language.PureScript.Traversals
5453
import Language.PureScript.TypeChecker.Deriving
5554
import Language.PureScript.TypeChecker.Entailment
5655
import Language.PureScript.TypeChecker.Kinds
@@ -369,38 +368,58 @@ 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+
-- when:
390+
-- ob { a = 0, b = 0 }
391+
--
392+
-- then:
393+
-- obTypes = [(a, ?0), (b, ?0)]
394+
obTypes <- zip updateLabels <$> replicateM (length updateLabels) (freshTypeWithKind kindType)
395+
let obItems :: [RowListItem SourceAnn]
396+
obItems = uncurry srcRowListItem <$> obTypes
397+
-- Create a record type that contains the unification variables.
398+
--
399+
-- obRecordType = Record ( a :: ?0, b :: ?0 | rowType )
400+
obRecordType :: SourceType
401+
obRecordType = srcTypeApp tyRecord $ rowFromList (obItems, rowType)
402+
-- Check ob against obRecordType.
403+
--
404+
-- when:
405+
-- ob : { a :: Int, b :: Int }
406+
--
407+
-- then:
408+
-- ?0 ~ Int
409+
-- ?1 ~ Int
410+
-- ob' : { a :: ?0, b :: ?1 }
411+
ob' <- TypedValue True <$> (tvToExpr <$> check ob obRecordType) <*> pure obRecordType
412+
-- Infer the types of the values used for the record update.
413+
typedFields <- inferProperties ps
414+
let newItems :: [RowListItem SourceAnn]
415+
newItems = (\(l, (_, t)) -> srcRowListItem (Label l) t) <$> typedFields
416+
417+
ps' :: [(PSString, Expr)]
418+
ps' = (\(l, (e, t)) -> (l, TypedValue True e t)) <$> typedFields
419+
420+
newRecordType :: SourceType
421+
newRecordType = srcTypeApp tyRecord $ rowFromList (newItems, rowType)
422+
pure $ TypedValue' True (ObjectUpdate ob' ps') newRecordType
404423
infer' (Accessor prop val) = withErrorMessageHint (ErrorCheckingAccessor val prop) $ do
405424
field <- freshTypeWithKind kindType
406425
rest <- freshTypeWithKind (kindRow kindType)
@@ -431,8 +450,7 @@ infer' v@(Constructor _ c) = do
431450
env <- getEnv
432451
case M.lookup c (dataConstructors env) of
433452
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'
453+
Just (_, _, ty, _) -> TypedValue' True v <$> (introduceSkolemScope <=< replaceAllTypeSynonyms $ ty)
436454
infer' (Case vals binders) = do
437455
(vals', ts) <- instantiateForBinders vals binders
438456
ret <- freshTypeWithKind kindType
@@ -474,6 +492,44 @@ infer' (PositionedValue pos c val) = warnAndRethrowWithPositionTC pos $ do
474492
return $ TypedValue' t (PositionedValue pos c v) ty
475493
infer' v = internalError $ "Invalid argument to infer: " ++ show v
476494

495+
-- |
496+
-- Infer the types of named record fields.
497+
inferProperties
498+
:: ( MonadSupply m
499+
, MonadState CheckState m
500+
, MonadError MultipleErrors m
501+
, MonadWriter MultipleErrors m
502+
)
503+
=> [(PSString, Expr)]
504+
-> m [(PSString, (Expr, SourceType))]
505+
inferProperties = traverse (traverse inferWithinRecord)
506+
507+
-- |
508+
-- Infer the type of a value when used as a record field.
509+
inferWithinRecord
510+
:: ( MonadSupply m
511+
, MonadState CheckState m
512+
, MonadError MultipleErrors m
513+
, MonadWriter MultipleErrors m
514+
)
515+
=> Expr
516+
-> m (Expr, SourceType)
517+
inferWithinRecord e = do
518+
TypedValue' _ v t <- infer e
519+
if propertyShouldInstantiate e
520+
then instantiatePolyTypeWithUnknowns v t
521+
else pure (v, t)
522+
523+
-- |
524+
-- Determines if an value's type needs to be monomorphized when
525+
-- used inside of a record.
526+
propertyShouldInstantiate :: Expr -> Bool
527+
propertyShouldInstantiate = \case
528+
Var{} -> True
529+
Constructor{} -> True
530+
PositionedValue _ _ e -> propertyShouldInstantiate e
531+
_ -> False
532+
477533
inferLetBinding
478534
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
479535
=> [Declaration]
@@ -795,7 +851,7 @@ check' v@(Constructor _ c) ty = do
795851
Nothing -> throwError . errorMessage . UnknownName . fmap DctorName $ c
796852
Just (_, _, ty1, _) -> do
797853
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
798-
ty' <- introduceSkolemScope ty
854+
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
799855
elaborate <- subsumes repl ty'
800856
return $ TypedValue' True (elaborate v) ty'
801857
check' (Let w ds val) ty = do
@@ -841,11 +897,11 @@ checkProperties expr ps row lax = convert <$> go ps (toRowPair <$> ts') r' where
841897
go ((p,v):ps') ts r =
842898
case lookup (Label p) ts of
843899
Nothing -> do
844-
v'@(TypedValue' _ _ ty) <- infer v
900+
(v', ty) <- inferWithinRecord v
845901
rest <- freshTypeWithKind (kindRow kindType)
846902
unifyTypes r (srcRCons (Label p) ty rest)
847903
ps'' <- go ps' ts rest
848-
return $ (p, v') : ps''
904+
return $ (p, TypedValue' True v' ty) : ps''
849905
Just ty -> do
850906
v' <- check v ty
851907
ps'' <- go ps' (delete (Label p, ty) ts) r

‎tests/purs/passing/4376.purs‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module Main where
2+
3+
import Prelude
4+
import Prim.Row (class Union)
5+
6+
import Effect.Console (log)
7+
import Type.Proxy (Proxy(..))
8+
9+
data Maybe a = Just a | Nothing
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+
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)