Opened 11 months ago

Last modified 8 weeks ago

#15831 new bug

DerivingVia allows bogus implicit quantification in `via` type

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

Description

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.

Change History (4)

comment:1 Changed 11 months ago by RyanGlScott

Milestone: 8.8.1

I think I see what's going on here. The aforementioned validity check is currently implemented in the renamer (in rnAndReportFloatingViaTvs), but the renamer is completely oblivious to the existence of inferred kind variables (such as k in the original example). This leads me to believe that the renamer is the wrong place to put this check, and that it should really live in the typechecker, where we do know about the existence of k.

comment:2 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:3 Changed 8 months ago by RyanGlScott

#16181 is likely a symptom of this ticket.

comment:4 Changed 8 weeks ago by Marge Bot <ben+marge-bot@…>

In 30b6f39/ghc:

Banish reportFloatingViaTvs to the shadow realm (#15831, #16181)

GHC used to reject programs of this form:

```
newtype Age = MkAge Int
  deriving Eq via Const Int a
```

That's because an earlier implementation of `DerivingVia` would
generate the following instance:

```
instance Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Note that the `a` in `Const Int a` is not bound anywhere, which
causes all sorts of issues. I figured that no one would ever want to
write code like this anyway, so I simply banned "floating" `via` type
variables like `a`, checking for their presence in the aptly named
`reportFloatingViaTvs` function.

`reportFloatingViaTvs` ended up being implemented in a subtly
incorrect way, as #15831 demonstrates. Following counsel with the
sage of gold fire, I decided to abandon `reportFloatingViaTvs`
entirely and opt for a different approach that would _accept_
the instance above. This is because GHC now generates this instance
instead:

```
instance forall a. Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Notice that we now explicitly quantify the `a` in
`instance forall a. Eq Age`, so everything is peachy scoping-wise.
See `Note [Floating `via` type variables]` in `TcDeriv` for the full
scoop.

A pleasant benefit of this refactoring is that it made it much easier
to catch the problem observed in #16181, so this patch fixes that
issue too.

Fixes #15831. Fixes #16181.
Note: See TracTickets for help on using tickets.