#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