0.15.0 won't completely infer types using VTA inside a record

Description

When using a value inside a record for which type depends on a type provided using the new VTA feature the compiler won't infer the type inside the record and instead leaves a forall. This then prevents other typeclasses like RowToList or Nub from working.

To Reproduce

module Example where

import Prelude

import Data.Reflectable (class Reflectable, reflectType)
import Type.Proxy (Proxy(..))

reflect :: forall @t v . Reflectable t v => v
reflect =
    reflectType ( Proxy @t )

use :: String
use =
    show { asdf : reflect @"asdf" }

Expected behavior

The code should compile and the value of use should be { asdf: "asdf" }

Additional context

The issue disappears when adding any other argument:

reflect :: forall @t v . Reflectable t v => Unit -> v
reflect _ =
    reflectType ( Proxy @t )

use :: String
use =
    show { asdf : reflect @"asdf" unit }

PureScript version

0.15.10

Posting the above code in Try PS: https://try.purescript.org/?code=FAWw9gJgrgNgpgAgLIEMCWA7BB3AFnAJzmGDRAAcwCAXBABSJigmNIqtoBEVqUA6AEpwAZvADGvAEbwEACjEwUAZyUIhouBJTS4AGgRENEgCoBPcnACUbSjQRmLfBmAAepuc7ey%2BfS9eCG4rQAXMEIwlQoMDAIAAK0AG4IfGoiQdoyiQgAvAB8CAkBaZq02cAIFQbFJuaIsvQEru7xCP5QSoihCADK1ASYAObA7YhllQhKuGDYCADeCMoQwghhgSVxAESLwhsIAL4kQA

Error is:

No type class instance was found for

    Prim.Row.Nub ( asdf :: forall v. Reflectable "asdf" v => v
                 )
                 ( asdf :: forall v. Reflectable "asdf" v => v
                 )


while solving type class constraint

  Data.Show.Show { asdf :: forall (v :: Type). Reflectable @Symbol "asdf" v => v
                 }

while applying a function show
  of type Show t0 => t0 -> String
  to argument { asdf: reflect
              }
while checking that expression show { asdf: reflect
                                    }
  has type String
in value declaration use

where t0 is an unknown type

#4376 introduced a typing rule for inferring property values inside of records:

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

Lines 549 to 573 in 4afea2f

    
           -- | 
        
           -- 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

The propertyShouldInstantiate function has been used for a while now but I don't exactly recall why it's there. Adding a special case for VisibleTypeApp should do the trick provided that the term being applied satisfies propertyShouldInstantiate too.

That fixes it. PR incoming.

Isn't this #4380 rearing it's head again? I think it's fine to special case VisibleTypeApp for now, but I still think we should just remove this rule.

I agree, but that's a breaking change, right?

Sunbelt Computer Software

PL/B Language Development and Support

Navigation Menu

Repository navigation

0.15.0 won't completely infer types using VTA inside a record #4500

Description

To Reproduce

Expected behavior

Additional context

PureScript version

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	-- \|
	-- 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

Sunbelt Computer Software

PL/B Language Development and Support

0.15.0 won't completely infer types using VTA inside a record #4500

Description

Description

To Reproduce

Expected behavior

Additional context

PureScript version

Activity

JordanMartinez commented on Aug 8, 2023

purefunctor commented on Aug 8, 2023

JordanMartinez commented on Aug 8, 2023

natefaubion commented on Aug 8, 2023

JordanMartinez commented on Aug 8, 2023

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions