Opened 12 months ago

Last modified 12 months ago

#15697 new bug

Typed holes inferring a more polymorphic type

Reported by: sreenidhi Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1
Keywords: TypedHoles Cc: Tritlo, ulysses4ever
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

Consider these two snippets.

testFailure :: Char
testFailure =
  let x = id _
  in  x

Suggestions provided were

/home/sreenidhi/Experiments/TypedHole.hs:3:14: error:
    • Found hole: _ :: a
      Where: ‘a’ is a rigid type variable bound by
               the inferred type of x :: a
               at /home/sreenidhi/Experiments/TypedHole.hs:3:7-14
    • In the first argument of ‘id’, namely ‘_’
      In the expression: id _
      In an equation for ‘x’: x = id _
    • Relevant bindings include
        x :: a (bound at /home/sreenidhi/Experiments/TypedHole.hs:3:7)
        testFailure :: Char
          (bound at /home/sreenidhi/Experiments/TypedHole.hs:2:1)

whereas for this one

testSuccess :: Char
testSuccess = _

It correctly suggests

/home/sreenidhi/Experiments/TypedHole.hs:7:15: error:
    • Found hole: _ :: Char
    • In the expression: _
      In an equation for ‘testSuccess’: testSuccess = _
    • Relevant bindings include
        testSuccess :: Char
          (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)
      Valid hole fits include
        testSuccess :: Char
          (bound at /home/sreenidhi/Experiments/TypedHole.hs:7:1)
        testFailure :: Char
          (defined at /home/sreenidhi/Experiments/TypedHole.hs:2:1)
        maxBound :: forall a. Bounded a => a
          with maxBound @Char
          (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1
           (and originally defined in ‘GHC.Enum’))
        minBound :: forall a. Bounded a => a
          with minBound @Char
          (imported from ‘Prelude’ at /home/sreenidhi/Experiments/TypedHole.hs:1:1
           (and originally defined in ‘GHC.Enum’))

Attachments (1)

TypedHole.hs (94 bytes) - added by sreenidhi 12 months ago.

Download all attachments as: .zip

Change History (8)

Changed 12 months ago by sreenidhi

Attachment: TypedHole.hs added

comment:1 Changed 12 months ago by RyanGlScott

Cc: Tritlo added
Keywords: TypedHoles added

comment:2 Changed 12 months ago by Tritlo

So, the suggestions here are correct (based on the type), but why is it not inferring that x is of type Char? It doesn't even look like it is inferring that a must end up being Char.

Last edited 12 months ago by Tritlo (previous) (diff)

comment:3 Changed 12 months ago by ulysses4ever

Cc: ulysses4ever added

comment:4 Changed 12 months ago by RyanGlScott

I suppose the correct behavior here depends on whether or not you want valid hole fit suggestions to suggest the most general type of local definitions or not. Consider the following modified example:

testFailure :: Char
testFailure =
  let x :: _
      x = id
  in x 'a'

You might think that the reported type of the hole would be Char -> Char, but it's actually forall a. a -> a. Indeed, forall a. a -> a is the most general type that you can give x, so from a certain perspective, it's the most "correct" answer. But perhaps it's not the one you'd desire.

One idea would be to allow tweaking the generalization behavior for local definitions à la MonoLocalBinds. For instance, in the following example:

testFailure2 :: Bool -> (Bool, Char)
testFailure2 x =
  let f y = (x, y)
  in f 'a'

If MonoLocalBinds isn't enabled, then the inferred type of f will be forall b. b -> (Bool, b). But if MonoLocalBinds is enabled, then the inferred type of f will be Char -> (Bool, Char).

I imagine we could allow valid hole fits to tweak generalization in a similar fashion (whether generalizing should be the default here or not is unclear to me).

comment:5 Changed 12 months ago by sreenidhi

I fully agree with your analysis about testFailure - for example I might want to write

test1 :: Char
test1 =
  let x :: _  -- now x really has to be forall a. a -> a
      x = id
  in const (x 'c') (x 5)

But consider the following

test2 :: Char
test2 =
  let x :: _    -- error: Found type wildcard ‘_’ standing for ‘Char’
      x = id 'c'
  in x

test3 :: Char
test3 =
  let x = id _ -- error: Found hole: _ :: a
  in x

Isn't it expected that the two errors to point to the same type?

comment:6 in reply to:  5 Changed 12 months ago by RyanGlScott

Replying to sreenidhi:

Isn't it expected that the two errors to point to the same type?

Again, that depends on whether you're generalizing or not. If you're generalizing, then forall a. a is what you'd expect as the type of that hole. (You could fill it with, say, undefined or let y = y in y.) If you're not generalizing, then Char would be what you would expect.

The bottom line is that we have a design choice here—there are situations where one behavior might be preferable over the other.

comment:7 Changed 12 months ago by Tritlo

Thanks for breaking it down, Ryan. I think this would be covered by what I call "more specific fits", like I touched on (i.e. suggesting pi :: Floating a => a for _ :: Fractional a => a). In those fits, we could also include fits that would be suggested if MonoLocalBinds were enabled.

Note: See TracTickets for help on using tickets.