Misleading Type Error

[BebeSparkelSparkel]

The compiler gives a misleading type error where it assumes the type should be Effect even though the top type declaration is Aff (line 19) then reports that an Aff line (line 24) is in error instead of the Effect line (line 22). I was having trouble simplifying this so I put the whole file, sorry.

  1 module ContentScript (main) where
  2
  3 import Prelude (Unit, bind, pure, (#), ($), (<#>), (>=>))
  4 import Effect (Effect)
  5 import Effect.Aff (Aff, launchAff_)
  6 import Effect.Class.Console (log, logShow)
  7 import Affjax as Affjax
  8 import Affjax.ResponseFormat as Res
  9 import Affjax.RequestBody as Req
 10 import Data.Either (Either(..), note)
 11 import Web.HTML.Window (prompt)
 12 import Web.HTML (window)
 13 import Effect.Class (class MonadEffect, liftEffect)
 14 import Control.Monad.Except.Trans (ExceptT(..), lift, runExceptT, withExceptT)
 15
 16 main :: Effect Unit
 17 main = launchAff_ $ logException mainEA
 18
 19 mainEA :: ExceptT String Aff Unit
 20 mainEA = do
 21   w <- lift $ liftEffect window
 22   promtval <- prompt "HI" w <#> note "Could not recived from prompt" # ExceptT -- line with type error
 23   let p = Affjax.post Res.string "http://localhost:9000" (pure $ Req.string promtval)
 24   res <- withExceptT Affjax.printError $ ExceptT p -- misleading compiler error line
 25   lift $ logShow res
 26
 27 logException :: forall m. MonadEffect m => ExceptT String m Unit -> m Unit
 28 logException = runExceptT >=> case _ of
 29   Right x -> pure x
 30   Left e -> log e
 31

Error found:
in module ContentScript
at src/ContentScript.purs:24:3 - 24:51 (line 24, column 3 - line 24, column 51)

  Could not match type

    Aff

  with type

    Effect


while trying to match type ExceptT String Aff
  with type ExceptT String Effect
while checking that expression (bind ((apply (...)) (ExceptT p))) (\res ->
                                                                     (apply lift) (logShow res)
                                                                  )
  has type ExceptT String Effect t0
in value declaration mainEA

where t0 is an unknown type

[milesfrain]

Here's a simplified example:

foo :: Effect Unit
foo = do
  log "hello"        -- Misleading compiler error here
  y <- Just "World"  -- This line should be flagged instead
  logShow y

https://try.purescript.org/?gist=1059a81d0a851f59bf6f3f641d5e0364

[natefaubion]

I think that having good errors for do-notation would probably require us to type-check the original do-syntax. I think it's likely that poor errors arise in do notation due to type-checking the desugared syntax, where conflicts in the tail propagate up the block. I'm not completely positive this is the case, but it's always been an issue even after we added correct source positions for this syntax.

[purefunctor]

I'd also like to note that using the monomorphized versions of log and logShow changes where the error squigglies appear. For this example, it appears on the logShow line instead:

foo :: Effect Unit
foo = do
  log "hello"
  y <- Just "World"  -- This line should be flagged instead
  logShow y          -- Misleading compiler error here

https://try.purescript.org/?gist=733fdfcc03328d2960d507200613d4e0

I do think type-check-then-desugar would definitely help produce better errors here, though.

[JordanMartinez]

That's what GHC does: type check, then desugar.

[rhendric]

Why wouldn't we change the order of operations in the type checker instead of type-checking sugared do blocks? Even with the manually desugared

foo :: Effect Unit
foo = log "hello" >>= \_ -> Just "World" >>= \y -> logShow y

we would want the Just "World" (in the monomorphic case) or the entire expression (in the polymorphic case) to receive the squiggly, wouldn't we?

I could be completely wrong about this but I would imagine that the type checker has some freedom when checking function applications to decide whether to unify instantiated result types with the expected type first or check arguments against the instantiated parameter types first, and I think that's the determining factor in where the squigglies end up, isn't it?

[purefunctor]

I could be completely wrong about this but I would imagine that the type checker has some freedom when checking function applications to decide whether to unify instantiated result types with the expected type first or check arguments against the instantiated parameter types first, and I think that's the determining factor in where the squigglies end up, isn't it?

Isn't it more like a synthesis rule? With checkFunctionApplication at least, it just returns the return type from an existing function arrow or just yields a unification variable.

[rhendric]

Yeah, I don't pretend to understand why the type checker is written the way it is, but it does seem to behave like—and this lines up with what I understand from the implementation—the algorithm when checking a function application is to first infer the function type, then check the argument against that type, and then check that the result of that type matches the expected type. I think that's basically Algorithm W's inference rule, with a unification step at the end for the final check. I'm asking if, when checking as opposed to inferring/synthesizing, it would make sense to reverse those steps: first, check the function against ?0 -> t, where t is the current expected type and ?0 is a new unknown; then check the argument against ?0 after applying substitutions. With multiple curried arguments, I would expect this variant algorithm to associate errors with earlier arguments in general, because the algorithm gets more type information before it checks the first argument in a chain of applications. But I don't know if this has downsides, especially when entailment and subsumption get involved.

[purefunctor]

I also can't say I understand bidirectional type checking thoroughly enough to diverge from the typing rules (which is currently 1-to-1 with the papers for the most part). I'm still leaning more towards adding more meta-information to the type checker by deferring the desugaring of do-blocks; we could always add special cases in the type checker, but that's not really maintainable 😄

[rhendric]

I don't think this is an issue specific to do blocks, though. See my earlier example; currently, the logShow expression is presented as the error, and I think there's a good argument for showing the error on the Just expression instead. In general, I think it'd be preferable to have a type checking algorithm that presents a unification error on the lexically earliest subexpression involved.

Edit: I should qualify that last statement, because it's not literally what I want. What I want is something more like, the type checker should present unification errors as if it were traversing an expression in normal order, building up a human-level understanding of the types involved, and presenting an error on the first inconsistency thus encountered.

In particular, with

data Trio a = Trio a a a

x = Trio false 0 ""

I would expect 0 to be highlighted (even though false is technically the earlier subexpression involved with the error, because Trio false is still a consistent ‘expression prefix’). But with

y :: Trio Unit
y = Trio false 0 ""

I would expect false to be highlighted, because at that point you know you aren't getting a Trio Unit. (In no case do I expect "" to be the first subexpression highlighted.)

The current algorithm highlights 0 in both cases, which I think is suboptimal and the root of this issue.

[purefunctor]

Ah, thanks for the clarification; that's a more intuitive way to look at it. I think more meta information when typing applications is the way to go then. As in, treating applications as a whole in order to figure out which argument position fails, while (edit: mostly) keeping the typing rule for function applications.

Edit: I see that this has to do with the type checker switching to inference while checking the type application, right? With your example, what happens is:

check (Trio false 0 "") (Trio Unit)
infer (Trio false 0) -> checkApp ""
  infer (Trio false) -> checkApp 0
    infer Trio -> checkApp false
    -- at this point, `a` should be `Boolean`