724ac1d · rowtype-yoga/purescript-native

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

Fix #1570

commit724ac1d684c57df54a3e3825b43c46418b16ae42 authorPhil Freeman <paf31@cantab.net> dateMon 26 Oct 2015, 11:28 (11 years ago) parent2c7f092

7 files changed+33−12

compare with golang

unifiedsplit

examples/failing/1570.purs+6 examples/passing/1570.purs+6 psci/PSCi.hs+1−1 src/Language/PureScript/TypeChecker.hs+1−1 src/Language/PureScript/TypeChecker/Kinds.hs+2−2 src/Language/PureScript/TypeChecker/Skolems.hs+9−4 src/Language/PureScript/TypeChecker/Types.hs+8−4

examples/failing/1570.pursnew file+6

@@ -0,0 +1,6 @@

1+-- @shouldFailWith ExpectedType

2+module M where

4+data F a = F a

6+test = \(x :: F) -> x

examples/passing/1570.pursnew file+6

@@ -0,0 +1,6 @@

1+module Main where

3+test :: forall a. a -> a

4+test = \(x :: a) -> x

6+main = Control.Monad.Eff.Console.log "Done"

psci/PSCi.hs+1−1

@@ -425,7 +425,7 @@ handleKindOf typ = do

425425 case M.lookup (P.Qualified (Just mName) $ P.ProperName "IT") (P.typeSynonyms env') of

426426 Just (_, typ') -> do

427427 let chk = P.CheckState env' 0 0 (Just mName)

428− k = fst . runWriter . runExceptT $ L.runStateT (P.unCheck (P.kindOf mName typ')) chk

428+ k = fst . runWriter . runExceptT $ L.runStateT (P.unCheck (P.kindOf typ')) chk

429429 case k of

430430 Left errStack -> PSCI . outputStrLn . P.prettyPrintMultipleErrors False $ errStack

431431 Right (kind, _) -> PSCI . outputStrLn . P.prettyPrintKind $ kind

src/Language/PureScript/TypeChecker.hs+1−1

@@ -206,7 +206,7 @@ typeCheckAll moduleName _ ds = mapM go ds <* mapM_ checkOrphanFixities ds

206206 go (d@(ExternDeclaration name ty)) = do

207207 warnAndRethrow (addHint (ErrorInForeignImport name)) $ do

208208 env <- getEnv

209− kind <- kindOf moduleName ty

209+ kind <- kindOf ty

210210 guardWith (errorMessage (ExpectedType ty kind)) $ kind == Star

211211 case M.lookup (moduleName, name) (names env) of

212212 Just _ -> throwError . errorMessage $ RedefinedIdent name

src/Language/PureScript/TypeChecker/Kinds.hs+2−2

@@ -76,8 +76,8 @@ instance Unifiable Check Kind where

7676-- |

7777-- Infer the kind of a single type

7878--

79−kindOf :: ModuleName -> Type -> Check Kind

80−kindOf _ ty = fst <$> kindOfWithScopedVars ty

79+kindOf :: Type -> Check Kind

80+kindOf ty = fst <$> kindOfWithScopedVars ty

8181

8282-- |

8383-- Infer the kind of a single type, returning the kinds of any scoped type variables

src/Language/PureScript/TypeChecker/Skolems.hs+9−4

@@ -72,11 +72,16 @@ skolemize ident sko scope = replaceTypeVars ident (Skolem ident sko scope)

7272-- only example of scoped type variables.

7373--

7474skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr

75−skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f

75+skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id onExpr onBinder in f

7676 where

77− go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

78− go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)

79− go other = other

77+ onExpr :: Expr -> Expr

78+ onExpr (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

79+ onExpr (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)

80+ onExpr other = other

81+

82+ onBinder :: Binder -> Binder

83+ onBinder (TypedBinder ty b) = TypedBinder (skolemize ident sko scope ty) b

84+ onBinder other = other

8085

8186-- |

8287-- Ensure skolem variables do not escape their scope

src/Language/PureScript/TypeChecker/Types.hs+8−4

@@ -373,11 +373,15 @@ inferBinder val (NamedBinder name binder) = do

373373 return $ M.insert name val m

374374inferBinder val (PositionedBinder pos _ binder) =

375375 warnAndRethrowWithPosition pos $ inferBinder val binder

376−-- TODO: When adding support for polymorphic types, check subsumption here

377−-- and change the definition of `binderRequiresMonotype`

376+-- TODO: When adding support for polymorphic types, check subsumption here,

377+-- change the definition of `binderRequiresMonotype`,

378+-- and use `kindOfWithScopedVars`.

378379inferBinder val (TypedBinder ty binder) = do

379− ty' <- replaceAllTypeSynonyms ty

380− val =?= ty' >> inferBinder val binder

380+ ty1 <- replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty

381+ kind <- liftCheck $ kindOf ty1

382+ checkTypeKind ty1 kind

383+ val =?= ty1

384+ inferBinder val binder

381385

382386-- | Returns true if a binder requires its argument type to be a monotype.

383387-- | If this is the case, we need to instantiate any polymorphic types before checking binders.