Opened 12 months ago

Last modified 9 months ago

#15677 new bug

Valid hole fits and GADT type variable names

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.6.1
Keywords: TypedHoles, GADTs Cc: Tritlo
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #9091 Differential Rev(s):
Wiki Page:

Description

Consider the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind

data HList :: [Type] -> Type where
 HNil  :: HList '[]
 HCons :: x -> HList xs -> HList (x:xs)

foo :: HList a -> HList a
foo HNil = HNil
foo (HCons (b :: bType) bs) = HCons _ bs

Here is the suggestion that the typed hole in foo provides:

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo              ( Bug.hs, Bug.o )

Bug.hs:16:37: error:
    • Found hole: _ :: x
      Where: ‘x’ is a rigid type variable bound by
               a pattern with constructor:
                 HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
               in an equation for ‘foo’
               at Bug.hs:16:6-26
    • In the first argument of ‘HCons’, namely ‘_’
      In the expression: HCons _ bs
      In an equation for ‘foo’: foo (HCons (b :: bType) bs) = HCons _ bs
    • Relevant bindings include
        bs :: HList xs (bound at Bug.hs:16:25)
        b :: x (bound at Bug.hs:16:13)
        foo :: HList a -> HList a (bound at Bug.hs:15:1)
      Constraints include a ~ (x : xs) (from Bug.hs:16:6-26)
      Valid hole fits include b :: x (bound at Bug.hs:16:13)
   |
16 | foo (HCons (b :: bType) bs) = HCons _ bs
   |                                     ^

One thing immediately stands out here: the hole has type x, but x appears no where in the definition of foo! I had expected this suggestion to mention bType, since I went through the effort of declaring b to have that type through a pattern signature, but GHC instead uses types from the definition of the HCons constructor itself. This seems less than ideal, since one would expect GHC to only ever mention types that are lexically in scope at a particular definition site.

One thing which complicates this idea is that there can be multiple in-scope type variables that all refer to the same type. For instance, if I define this function:

bar :: HList a -> HList a -> HList a
bar HNil HNil = HNil
bar (HCons (b :: bType) bs) (HCons (c :: cType) cs) = HCons _ bs

What should the suggested type of the hole be: bType, or cType? Either choice is equally valid. After talking with Tritlo and simonpj about this, we came to the consensus that we should just pick one of the type variables to report at the top of the error message:

    • Found hole: _ :: bType

And then later in the message, include any type variable synonyms that have been brought into scope (via pattern signatures or otherwise). I imagine this might look something like:

    • Type variable synonyms include
        `cType` equals `bType`

This is quite similar to an existing feature of valid hole fits where we report Constraints include. (Indeed, we briefly considered just reporting these type variable synonyms as explicit equality constraints, but doing so would be somewhat misleading, since that's not how pattern signatures actually work in practice.)

One implementation challenge is to figure out how to construct a mapping from x to bType. One place where inspiration can be drawn from is the ATyVar constructor of TcTyThing:

data TcTyThing
  = ...
  | ATyVar  Name TcTyVar        -- The type variable to which the lexically scoped type
                                -- variable is bound. We only need the Name
                                -- for error-message purposes; it is the corresponding
                                -- Name in the domain of the envt

ATyVar already stores a "reverse mapping" of sorts to give better a more accurate Name in the event that it is pretty-printed, which is quite similar to what we need to do with x and bType.

Change History (5)

comment:1 Changed 9 months ago by RyanGlScott

Example 3 in #9091 is likely another example of this phenomenon:

data X a where
  Y :: X Int

h :: X a -> a -> a
h Y x = _
    Found hole ‘_’ with type: Int
    Relevant bindings include
      x :: a (bound at THC.hs:13:5)
      h :: X a -> a -> a (bound at THC.hs:13:1)
    In the expression: _
    In an equation for ‘h’: h Y x = _

Note that in the list of relevant bindings, in reports that x is of type a, although it would be more informative to report it as having type Int due to the GADT pattern match.

comment:2 Changed 9 months ago by Tritlo

Well, at least the situation for #9091 is a bit better now, with constraints shown by default:

tritlo@nietzsche:~/Code$ ghc t9091.hs -XGADTs
[1 of 1] Compiling T9091            ( t9091.hs, t9091.o )

t9091.hs:7:9: error:
    • Found hole: _ :: Int
    • In the expression: _
      In an equation for ‘h’: h Y x = _
    • Relevant bindings include
        x :: a (bound at t9091.hs:7:5)
        h :: X a -> a -> a (bound at t9091.hs:7:1)
      Constraints include a ~ Int (from t9091.hs:7:3)
      Valid hole fits include
        x :: a (bound at t9091.hs:7:5)
        maxBound :: forall a. Bounded a => a
          with maxBound @Int
          (imported from ‘Prelude’ at t9091.hs:1:8-12
           (and originally defined in ‘GHC.Enum’))
        minBound :: forall a. Bounded a => a
          with minBound @Int
          (imported from ‘Prelude’ at t9091.hs:1:8-12
           (and originally defined in ‘GHC.Enum’))
  |
7 | h Y x = _

but this is still an issue.

comment:3 Changed 9 months ago by RyanGlScott

Oops! I missed the a ~ Int part. Indeed, that's much better (and I might even go as far as saying that that fixes that particular buglet).

comment:4 Changed 9 months ago by Tritlo

Interestingly, it also works for example 1 in #9091, but not for example 2 (possibly because a0 is made up by the type checker?). So if we fix that, we can at least close #9091.

comment:5 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.