Opened 10 months ago

Last modified 6 months ago

#14722 new feature request

Error message points to wrong location

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: TypeApplications, DeferredErrors Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This rightly fails, but I have an issue with the error message. I think points to the visible type application eagerly.. rather than the type annotation (f_xx :: ()).

{-# Language RankNTypes, PolyKinds, GADTs, TypeApplications, ScopedTypeVariables #-}

import Data.Kind

newtype Limit :: (k -> Type) -> Type where
  Limit :: (forall xx. f xx) -> Limit f

foo :: forall f a. Limit f -> f a
foo (Limit (f_xx :: ())) = f_xx @a

gives

$ ghci -ignore-dot-ghci /tmp/Test.hs 
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Test.hs, interpreted )

/tmp/Test.hs:9:28: error:
    • Cannot apply expression of type ‘()’
      to a visible type argument ‘a’
    • In the expression: f_xx @a
      In an equation for ‘foo’: foo (Limit (f_xx :: ())) = f_xx @a
  |
9 | foo (Limit (f_xx :: ())) = f_xx @a
  |                            ^^^^^^^
Failed, no modules loaded.
Prelude> 

I would have expected:

/tmp/Test.hs:9:13: error:
    • Couldn't match expected type ‘()’ with actual type ‘f xx0’
    • When checking that the pattern signature: ()
        fits the type of its context: forall (xx :: k1). f xx
      In the pattern: f_xx :: ()
      In the pattern: Limit (f_xx :: ())
    • Relevant bindings include
        foo :: Limit f -> f a (bound at /tmp/Test.hs:9:1)

Thoughts

Change History (3)

comment:1 Changed 10 months ago by simonpj

Keywords: TypeApplications added

You're right. This is a consequence of the fact that (currently) GHC reports visible-type-application errors "eagerly", as soon as it encounters them, discarding all pending errors. In this case the error you want reported will be pending (in the constraints being gathered) but it never gets a chance to be reported.

Richard: it'd be good to find a way to defer the visible-type-application error. But we don't have a way to do that yet. A HoleCan isn't right. A constraint [W] () ~ forall a. ??? doesn't seem right because we have nothing to put for the ??. I suppose we could invent a new kind of deferred error constraint, perhaps generalising HoleCan.

See TypeApplication for a list of other VTA-related tickets; I have not checked but I bet that some are like this one.

comment:2 Changed 10 months ago by goldfire

Yes, I think that's the right approach, in order to get this error to interact better with others.

comment:3 Changed 6 months ago by simonpj

Keywords: DeferredErrors added
Note: See TracTickets for help on using tickets.