9376fdc · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

on golang help sign in

Fix function application judgment

9376fdcPhil Freeman10 years ago

examples/failing/DoNotSuggestComposition2.purs+1−1

compare with golang

unifiedsplit

@@ -1,4 +1,4 @@

1−-- @shouldFailWith CannotApplyFunction

1+-- @shouldFailWith TypesDoNotUnify

2-- TODO: Check that this does not produce a "function composition is (<<<)"

3-- suggestion.

examples/failing/OperatorSections.purs+1−2

@@ -1,8 +1,7 @@

1−-- @shouldFailWith CannotApplyFunction

1+-- @shouldFailWith TypesDoNotUnify

2module Main where

4import Prelude

6main = do

7 (true `not` _)

8−

src/Language/PureScript/AST/Declarations.hs−1

@@ -90,7 +90,6 @@ data SimpleErrorMessage

90 | ExprDoesNotHaveType Expr Type

91 | PropertyIsMissing String

92 | AdditionalProperty String

93− | CannotApplyFunction Type Expr

94 | TypeSynonymInstance

93 | TypeSynonymInstance

95 | OrphanInstance Ident (Qualified (ProperName 'ClassName)) [Type]

94 | OrphanInstance Ident (Qualified (ProperName 'ClassName)) [Type]

96 | InvalidNewtype (ProperName 'TypeName)

95 | InvalidNewtype (ProperName 'TypeName)

src/Language/PureScript/Errors.hs−12

@@ -133,7 +133,6 @@ errorCode em = case unwrapErrorMessage em of

133 ExprDoesNotHaveType{} -> "ExprDoesNotHaveType"

134 PropertyIsMissing{} -> "PropertyIsMissing"

135 AdditionalProperty{} -> "AdditionalProperty"

136− CannotApplyFunction{} -> "CannotApplyFunction"

137 TypeSynonymInstance -> "TypeSynonymInstance"

136 TypeSynonymInstance -> "TypeSynonymInstance"

138 OrphanInstance{} -> "OrphanInstance"

137 OrphanInstance{} -> "OrphanInstance"

139 InvalidNewtype{} -> "InvalidNewtype"

138 InvalidNewtype{} -> "InvalidNewtype"

@@ -257,7 +256,6 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse

257 gSimple (TypesDoNotUnify t1 t2) = TypesDoNotUnify <$> f t1 <*> f t2

256 gSimple (TypesDoNotUnify t1 t2) = TypesDoNotUnify <$> f t1 <*> f t2

258 gSimple (ConstrainedTypeUnified t1 t2) = ConstrainedTypeUnified <$> f t1 <*> f t2

257 gSimple (ConstrainedTypeUnified t1 t2) = ConstrainedTypeUnified <$> f t1 <*> f t2

259 gSimple (ExprDoesNotHaveType e t) = ExprDoesNotHaveType e <$> f t

258 gSimple (ExprDoesNotHaveType e t) = ExprDoesNotHaveType e <$> f t

260− gSimple (CannotApplyFunction t e) = CannotApplyFunction <$> f t <*> pure e

261 gSimple (InvalidInstanceHead t) = InvalidInstanceHead <$> f t

259 gSimple (InvalidInstanceHead t) = InvalidInstanceHead <$> f t

262 gSimple (NoInstanceFound con) = NoInstanceFound <$> overConstraintArgs (traverse f) con

260 gSimple (NoInstanceFound con) = NoInstanceFound <$> overConstraintArgs (traverse f) con

263 gSimple (OverlappingInstances cl ts insts) = OverlappingInstances cl <$> traverse f ts <*> pure insts

261 gSimple (OverlappingInstances cl ts insts) = OverlappingInstances cl <$> traverse f ts <*> pure insts

@@ -691,12 +689,6 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS

691 line $ "Type of expression lacks required label " ++ markCode prop ++ "."

689 line $ "Type of expression lacks required label " ++ markCode prop ++ "."

692 renderSimpleErrorMessage (AdditionalProperty prop) =

690 renderSimpleErrorMessage (AdditionalProperty prop) =

693 line $ "Type of expression contains additional label " ++ markCode prop ++ "."

691 line $ "Type of expression contains additional label " ++ markCode prop ++ "."

694− renderSimpleErrorMessage (CannotApplyFunction fn arg) =

695− paras [ line "A function of type"

696− , markCodeBox $ indent $ typeAsBox fn

697− , line "can not be applied to the argument"

698− , markCodeBox $ indent $ prettyPrintValue valueDepth arg

699− ]

700 renderSimpleErrorMessage TypeSynonymInstance =

692 renderSimpleErrorMessage TypeSynonymInstance =

701 line "Type class instances for type synonyms are disallowed."

693 line "Type class instances for type synonyms are disallowed."

702 renderSimpleErrorMessage (OrphanInstance nm cnm ts) =

694 renderSimpleErrorMessage (OrphanInstance nm cnm ts) =

@@ -1036,10 +1028,6 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS

1036

1028

1037 -- | See https://github.com/purescript/purescript/issues/1802

1029 -- | See https://github.com/purescript/purescript/issues/1802

1038 stripRedudantHints :: SimpleErrorMessage -> [ErrorMessageHint] -> [ErrorMessageHint]

1030 stripRedudantHints :: SimpleErrorMessage -> [ErrorMessageHint] -> [ErrorMessageHint]

1039− stripRedudantHints CannotApplyFunction{} = stripFirst isApplicationHint

1040− where

1041− isApplicationHint ErrorInApplication{} = True

1042− isApplicationHint _ = False

1043 stripRedudantHints ExprDoesNotHaveType{} = stripFirst isCheckHint

1031 stripRedudantHints ExprDoesNotHaveType{} = stripFirst isCheckHint

1044 where

1032 where

1045 isCheckHint ErrorCheckingType{} = True

1033 isCheckHint ErrorCheckingType{} = True

src/Language/PureScript/TypeChecker/Types.hs+53−41

@@ -292,7 +292,7 @@ infer' (Abs (Left arg) ret) = do

292infer' (Abs (Right _) _) = internalError "Binder was not desugared"

293infer' (App f arg) = do

294 f'@(TypedValue _ _ ft) <- infer f

295− (ret, app) <- checkFunctionApplication f' ft arg Nothing

295+ (ret, app) <- checkFunctionApplication f' ft arg

296 return $ TypedValue True app ret

297infer' (Var var) = do

298 checkVisibility var

@@ -567,8 +567,11 @@ check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) = do

567check' (Abs (Right _) _) _ = internalError "Binder was not desugared"

568check' (App f arg) ret = do

569 f'@(TypedValue _ _ ft) <- infer f

570− (_, app) <- checkFunctionApplication f' ft arg (Just ret)

570+ (retTy, app) <- checkFunctionApplication f' ft arg

571+ v' <- subsumes (Just app) retTy ret

572+ case v' of

573+ Nothing -> internalError "check: unable to check the subsumes relation."

571− return $ TypedValue True app ret

574+ Just app' -> return $ TypedValue True app' ret

572check' v@(Var var) ty = do

575check' v@(Var var) ty = do

573 checkVisibility var

576 checkVisibility var

574 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var

577 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable $ var

@@ -692,55 +695,64 @@ checkProperties expr ps row lax = let (ts, r') = rowToList row in go ps ts r' wh

692 return $ (p, v') : ps''

695 return $ (p, v') : ps''

693 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyRecord row)

696 go _ _ _ = throwError . errorMessage $ ExprDoesNotHaveType expr (TypeApp tyRecord row)

694

697

695−-- | Check the type of a function application, rethrowing errors to provide a better error message

698+-- | Check the type of a function application, rethrowing errors to provide a better error message.

696−checkFunctionApplication ::

699+--

700+-- This judgment takes three inputs:

701+--

702+-- * The expression of the function we are applying

703+-- * The type of that function

704+-- * The expression we are applying it to

705+--

706+-- and synthesizes two outputs:

707+--

708+-- * The return type

709+-- * The elaborated expression for the function application (since we might need to

710+-- insert type class dictionaries, etc.)

711+checkFunctionApplication

697− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

712+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

698− Expr ->

713+ => Expr

699− Type ->

714+ -- ^ The function expression

715+ -> Type

716+ -- ^ The type of the function

700− Expr ->

717+ -> Expr

701− Maybe Type ->

718+ -- ^ The argument expression

702− m (Type, Expr)

719+ -> m (Type, Expr)

720+ -- ^ The result type, and the elaborated term

703−checkFunctionApplication fn fnTy arg ret = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do

721+checkFunctionApplication fn fnTy arg = withErrorMessageHint (ErrorInApplication fn fnTy arg) $ do

704 subst <- gets checkSubstitution

722 subst <- gets checkSubstitution

705− checkFunctionApplication' fn (substituteType subst fnTy) arg (substituteType subst <$> ret)

723+ checkFunctionApplication' fn (substituteType subst fnTy) arg

706

724

707-- | Check the type of a function application

725-- | Check the type of a function application

708−checkFunctionApplication' ::

726+checkFunctionApplication'

709− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>

727+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

710− Expr ->

728+ => Expr

711− Type ->

729+ -> Type

712− Expr ->

730+ -> Expr

713− Maybe Type ->

714− m (Type, Expr)

731+ -> m (Type, Expr)

715−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do

732+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do

716 unifyTypes tyFunction' tyFunction

733 unifyTypes tyFunction' tyFunction

717 arg' <- check arg argTy

734 arg' <- check arg argTy

718− case ret of

719− Nothing -> return (retTy, App fn arg')

735+ return (retTy, App fn arg')

720− Just ret' -> do

721− Just app' <- subsumes (Just (App fn arg')) retTy ret'

722− return (retTy, app')

723−checkFunctionApplication' fn (ForAll ident ty _) arg ret = do

736+checkFunctionApplication' fn (ForAll ident ty _) arg = do

724 replaced <- replaceVarWithUnknown ident ty

737 replaced <- replaceVarWithUnknown ident ty

725− checkFunctionApplication fn replaced arg ret

738+ checkFunctionApplication fn replaced arg

726−checkFunctionApplication' fn u@(TUnknown _) arg ret = do

739+checkFunctionApplication' fn (KindedType ty _) arg =

740+ checkFunctionApplication fn ty arg

741+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do

742+ dicts <- getTypeClassDictionaries

743+ hints <- gets checkHints

744+ checkFunctionApplication' (foldl App fn (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) fnTy arg

745+checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} =

746+ return (fnTy, App fn dict)

747+checkFunctionApplication' fn u arg = do

727 arg' <- do

748 arg' <- do

728 TypedValue _ arg' t <- infer arg

749 TypedValue _ arg' t <- infer arg

729 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t

750 (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t

730 return $ TypedValue True arg'' t'

751 return $ TypedValue True arg'' t'

731 let ty = (\(TypedValue _ _ t) -> t) arg'

752 let ty = (\(TypedValue _ _ t) -> t) arg'

732− ret' <- maybe freshType return ret

753+ ret <- freshType

733− unifyTypes u (function ty ret')

754+ unifyTypes u (function ty ret)

734− return (ret', App fn arg')

755+ return (ret, App fn arg')

735−checkFunctionApplication' fn (KindedType ty _) arg ret =

736− checkFunctionApplication fn ty arg ret

737−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do

738− dicts <- getTypeClassDictionaries

739− hints <- gets checkHints

740− checkFunctionApplication' (foldl App fn (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) fnTy arg ret

741−checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =

742− return (fnTy, App fn dict)

743−checkFunctionApplication' _ fnTy arg _ = throwError . errorMessage $ CannotApplyFunction fnTy arg

744

756

745-- |

757-- |

746-- Ensure a set of property names and value does not contain duplicate labels

758-- Ensure a set of property names and value does not contain duplicate labels