Opened 4 years ago

Last modified 18 months ago

#11186 new feature request

Give strong preference to type variable names in scope when reporting hole contexts

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.2
Keywords: TypedHoles Cc: goldfire, sweirich, adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

When using ScopedTypeVariables with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like

foo :: forall bar . ...
foo = ... _ ...

and yet the typed hole message shows that bar has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.

Change History (9)

comment:1 Changed 4 years ago by simonpj

Can you give a concrete example?

comment:2 in reply to:  1 Changed 4 years ago by dfeuer

Replying to simonpj:

Can you give a concrete example?

I finally found one, attempting to figure out how to write something like reverse for type-aligned lists. In this case, I use a pattern signature to name an existentially quantified type, but GHC's message doesn't seem to respect that.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module TAList where
import Control.Category
import Prelude hiding ((.), id)

data TAList (cat :: k -> k -> *) (x :: k) (z :: k) where
   Nil :: TAList cat x x
   (:<) :: cat b c -> TAList cat a b -> TAList cat a c
infixr 5 :<

newtype Op cat x y = Op {op :: cat y x}

reverseOntoTA :: TAList cat b d -> TAList (Op cat) d a -> TAList (Op cat) d a
reverseOntoTA Nil ys = ys
reverseOntoTA ((x :: cat c d) :< (xs :: TAList cat b c)) ys = _

I named the unknown type variable c, but GHC says:

    Relevant bindings include
      ys :: TAList (Op cat) d a (bound at TAList.hs:32:58)
      xs :: TAList cat b b1 (bound at TAList.hs:32:35)
      x :: cat b1 d (bound at TAList.hs:32:17)
      reverseOntoTA :: TAList cat b d
                       -> TAList (Op cat) d a -> TAList (Op cat) d a

That is, it's decided to name that variable b1 instead.

comment:3 Changed 4 years ago by dfeuer

It looks like it may be preferring the name of the type variable used in the GADT definition to the one in the pattern, which seems very wrong to me.

comment:4 Changed 4 years ago by dfeuer

Now that I know what to look for, I found a much smaller example:

{-# LANGUAGE ExistentialTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

data Foop = forall xx . Foop xx

blah (Foop (q :: pah)) = _

Here GHC again ignores the requested pah variable in favor of xx.

comment:5 Changed 4 years ago by simonpj

OK I understand. Here is a version of comment:4 that actually shows the problem

{-# LANGUAGE ExistentialQuantification, ScopedTypeVariables #-}
module T11186 where
  data Foop = forall xx . Foop xx
  blah (Foop (q :: pah)) = length ([q] :: _)

We get

T11186.hs:8:41: error:
    • Found type wildcard ‘_’ standing for ‘[xx]’
      Where: ‘xx’ is a rigid type variable bound by
               a pattern with constructor: Foop :: forall xx. xx -> Foop,
               in an equation for ‘blah’
               at T11186.hs:8:7

Now, the difficulty is this: lexically scoped type variable might be bound somewhere very different to the existential pattern itself. For example:

bla2 (Foop q) = (\(r::pah) -> length ([r] :: _)) q

And indeed, the same skolem bound in the pattern might have different lexical names in different places:

bla2 (Foop q) = ( (\(r::pah) -> length ([r] :: _)) q
                , (\(r::hap) -> length ([r] :: _)) q )

Now what would you expect?

Ugh. Tiresome, and not particularly easy to fix.

  • Visible type application will let you bind the type variable in the pattern (which is where it "ought" to be bound
  • Maybe some hack could do a better job when the type variable is in fact bound in the pattern where the existential is born.

Funnily enough, Richard, Stephanie, Adam, and I were discussing questions around lexically scoped type variables only last week.

comment:6 Changed 4 years ago by simonpj

Cc: goldfire sweirich adamgundry added

comment:7 in reply to:  5 Changed 3 years ago by dfeuer

Replying to simonpj:

And indeed, the same skolem bound in the pattern might have different lexical names in different places:

bla2 (Foop q) = ( (\(r::pah) -> length ([r] :: _x)) q
                , (\(r::hap) -> length ([r] :: _y)) q )

Now what would you expect?

I would expect the report about _x to tell me about pah and the one about _y to tell me about hap. May I ask what you think will be hard about this?

comment:8 Changed 3 years ago by simonpj

May I ask what you think will be hard about this?

Well, the message prints the type of [r], and the type is the same in both cases.

Your point, which is a reasonable one, is that you'd like the type to be rewritten to make sense in the current lexical context, whatever that is.

I don't think that would be too hard. The current lexical environment maps, say pah :-> t8, where t8 is the variable GHC chose for the argument type of q. So we could reverse-map back from t8 to pah.

Not hard, but more than the work of a moment. I can advise if someone wants to have a go.

Simon

comment:9 Changed 18 months ago by simonpj

Keywords: TypedHoles added; typed-holes removed
Note: See TracTickets for help on using tickets.