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.

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	Tritlo
Operating system
Architecture