[GHC] #15677: Valid hole fits and GADT type variable names

26 Sep 2018

      #15677: Valid hole fits and GADT type variable names
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.6.1
           Keywords:  TypedHoles,    |  Operating System:  Unknown/Multiple
  GADTs                              |
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following code:

 {{{#!hs
 {-# 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:

 {{{#!hs
 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`:

 {{{#!hs
 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`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15677
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler