DerivingVia allows bogus implicit quantification in `via` type

Consider the following code:

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE PolyKinds #-}
module Bug where

import Data.Functor.Const (Const(..))
import GHC.Exts (Any)

newtype Age = MkAge Int
  deriving Eq
    via Const Int Any

This fails to compile with a spectacularly unhelpful error message:

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

==================== Derived instances ====================
Derived class instances:
  instance GHC.Classes.Eq Bug.Age where
    (GHC.Classes.==)
      = GHC.Prim.coerce
          @((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
            -> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
               -> GHC.Types.Bool)
          @(Bug.Age -> Bug.Age -> GHC.Types.Bool)
          (GHC.Classes.==) ::
          Bug.Age -> Bug.Age -> GHC.Types.Bool
    (GHC.Classes./=)
      = GHC.Prim.coerce
          @((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
            -> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
               -> GHC.Types.Bool)
          @(Bug.Age -> Bug.Age -> GHC.Types.Bool)
          (GHC.Classes./=) ::
          Bug.Age -> Bug.Age -> GHC.Types.Bool
  

Derived type family instances:



Bug.hs:9:12: error:
    The exact Name ‘k’ is not in scope
      Probable cause: you used a unique Template Haskell name (NameU), 
      perhaps via newName, but did not bind it
      If that's it, then -ddump-splices might be useful
  |
9 |   deriving Eq
  |            ^^

Bug.hs:9:12: error:
    The exact Name ‘k’ is not in scope
      Probable cause: you used a unique Template Haskell name (NameU), 
      perhaps via newName, but did not bind it
      If that's it, then -ddump-splices might be useful
  |
9 |   deriving Eq
  |            ^^

Bug.hs:9:12: error:
    The exact Name ‘k’ is not in scope
      Probable cause: you used a unique Template Haskell name (NameU), 
      perhaps via newName, but did not bind it
      If that's it, then -ddump-splices might be useful
  |
9 |   deriving Eq
  |            ^^

Bug.hs:9:12: error:
    The exact Name ‘k’ is not in scope
      Probable cause: you used a unique Template Haskell name (NameU), 
      perhaps via newName, but did not bind it
      If that's it, then -ddump-splices might be useful
  |
9 |   deriving Eq
  |            ^^

There are two things that are strange here:

• Notice that in the derived Eq instance, there are references to (GHC.Types.Any :: k_a24l), where k_a24l is completely free! This should never happen, and is almost surely the cause of the resulting volley of errors.
• It's quite odd that we didn't reject this deriving clause outright //before// generating the derived code. In fact, if we explicitly mention the kind k:

newtype Age = MkAge Int
  deriving Eq
    via Const Int (Any :: k)

//Then// it's rejected properly:

$ /opt/ghc/8.6.1/bin/ghc Bug.hs          
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )                                              
                                                                                                   
Bug.hs:9:12: error:                                                                                
    Type variable ‘k’ is bound in the ‘via’ type ‘Const Int (Any :: k)’                            
    but is not mentioned in the derived class ‘Eq’, which is illegal                               
  |                                                                                                
9 |   deriving Eq                                                                                  
  |            ^^

Something about implicit quantification must be sneaking by this validity check.

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
Operating system
Architecture