Opened 11 months ago

Closed 9 months ago

#15828 closed bug (fixed)

Type family equation foralls allow strange re-quantification of class-bound type variables

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.7
Keywords: TypeFamilies Cc: mayac, simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: rename/should_fail/T15828
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5283
Wiki Page:

Description

The following code typechecks on GHC HEAD (8.7+):

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

class C1 a where
  type T1 a b
class C2 a where
  type T2 a b

instance C1 (Maybe a) where
  type forall a b. T1 (Maybe a) b = b
instance C2 (Maybe a) where
  type forall   b. T2 (Maybe a) b = b

But ought it to? There is something funny happening in the C1 instance: it's explicitly quantifying a, despite the fact that it had previously been quantified by the class head! Moreover, it appears that you can safely drop the a in the explicit forall, as the C2 (Maybe a) instance witnesses.

What does the documentation have to say on this topic? This is all I could find:

When an explicit forall is present, all type variables mentioned must be bound by the forall.

I couldn't find anything on the interaction between this feature and associated type families. We should:

  1. Decide which of the two programs above should be accepted, and
  2. Update the documentation to reflect this.

Change History (13)

comment:1 Changed 11 months ago by goldfire

Cc: mayac added

I vote strongly for C2. C1 should be rejected because the local a shadows the class-bound a, and so the associated type family equation doesn't match its template.

You forgot to mention that we need to

  1. Fix the implementation.

@mayac, do you want to see this (and any other oddities that pop up) through? Or would you prefer that others (perhaps me) fix any problems that arise?

comment:2 Changed 11 months ago by mayac

I also agree C1 should be rejected, though I'm quite baffled by why that is currently not the case. It appears that the two as in the C1 example truly do have the same name post-GhcRn. Shouldn't bindLHsTyVarBndrs be coming up with a fresh name for each explicitly quantified type variable anyway? I don't think I understand enough about the way GHC comes up with new names to see where this goes wrong...

In response to @goldfire, I would be happy to address these things as they come up! Of course, if someone finds a fix faster than I do they should feel free to go ahead with the change. In this case, I would need some guidance as I expressed above.

As for the documentation, how about the following:

When an explicit forall is present, all type variables mentioned which are not already in scope must be bound by the forall.

comment:3 Changed 11 months ago by goldfire

Shamefully, the answer is not to pass the mb_cls to the call to bindLHsTyVarBndrs in rnFamInstEqn -- always pass Nothing. If an associated class is passed in, then bindLHsTyVarBndrs uses the in-scope class variables, which is not what's wanted here. Really, only bindHsQTyVars should pass a non-Nothing in this parameter.

comment:4 Changed 11 months ago by mayac

Differential Rev(s): Phab:D5283

comment:5 Changed 11 months ago by mayac

@goldfire do you think it would be worth including in this fix a comment to the type signature of bindLHsTyVarBndrs mentioning that the mb_cls argument should usually be Nothing? For example:

 bindLHsTyVarBndrs :: HsDocContext
                   -> Maybe SDoc            -- Just d => check for unused tvs
                                            --   d is a phrase like "in the type ..."
                   -> Maybe a               -- Just _  => an associated type decl
+                                           -- (should be Nothing unless in bindHsQTyVars)
                   -> [LHsTyVarBndr GhcPs]  -- User-written tyvars
                   -> ([LHsTyVarBndr GhcRn] -> RnM (b, FreeVars))
                   -> RnM (b, FreeVars)

comment:6 Changed 11 months ago by goldfire

I've answered comment:5 on Phab:D5283

comment:7 Changed 10 months ago by Ryan Scott <ryan.gl.scott@…>

In fe57a5ba/ghc:

Fix #15828, from `More explicit foralls`

Summary:
Fix a bug in commit 12eeb9 which permits the following:

```
class C a where
  type T a b
instance C (Maybe a) where
  type forall a b. T (Maybe a) b = b
```

where instead, the user should write:

```
instance C (Maybe a) where
  type forall b. T (Maybe a) b = b
```

Update the users guide to discuss scoping of type variables in
explicit foralls in type family instances.

Test Plan: validate

Reviewers: bgamari, goldfire, monoidal

Reviewed By: goldfire

Subscribers: monoidal, rwbarton, carter

GHC Trac Issues: #15828

Differential Revision: https://phabricator.haskell.org/D5283

comment:8 Changed 10 months ago by RyanGlScott

Milestone: 8.8.1
Resolution: fixed
Status: newclosed
Test Case: rename/should_fail/T15828

comment:9 Changed 10 months ago by RyanGlScott

Cc: simonpj added
Resolution: fixed
Status: closednew

Hm... I might have been a little too hasty in closing this ticket. This patch was undoubtedly an improvement over the status quo, as we now throw a proper error instead of silently accepting the original program. However, the error message leaves something to be desired:

T15828.hs:9:3: error:
    • Type indexes must match class instance head
      Expected: T (Maybe a) _
        Actual: T (Maybe a) b -- Defined at T15828.hs:9:20
    • In the type instance declaration for ‘T’
      In the instance declaration for ‘C (Maybe a)’

Why did this fail? It's extremely hard to tell, but it's because the two a variables aren't the same! I suspect that we're missing some necessary tidying here.

Simon, this behavior appears to be new as of your commit 2257a86daa72db382eb927df12a718669d5491f8 (Taming the Kind Inference Monster). In particular, this change looks suspicious:

+    pp_expected_ty = pprIfaceType (toIfaceType (mkTyConApp fam_tc expected_args))
+                     -- Do /not/ tidy, because that will rename all those "_"
+                     -- variables we have put in.  And (I think) the intance type
+                     --  is already tidy

comment:10 Changed 10 months ago by simonpj

Fix a bug in commit 12eeb9 which permits the following:

What is 12eeb9?

$ git show 12eeb9  
fatal: ambiguous argument '12eeb9': unknown revision or path not in the working tree.

(In an up to date tree.)

hy did this fail? It's extremely hard to tell, but it's because the two a variables aren't the same!

Quite true. So what would we like to show here? Once we decide that we can think how to achieve it. (It is perhaps fortunate that there is a dedicated pretty-printer for this particular error.)

I'm quite keen on using "_" for the bits that don't matter, but if needs must, instead of printing (F t1 t2 t3) with one call, we can make separate calls for t1, t2, t3 etc, and that would eliminate the need to fake-up a tyvar "_" which you'll see in the code.

Would love to have your help if here if you are willing.

comment:11 in reply to:  10 Changed 10 months ago by RyanGlScott

Replying to simonpj:

What is 12eeb9?

It's referring to commit 512eeb9bb9a81e915bfab25ca16bc87c62252064 (the leading "5" was simply dropped by mistake).

Quite true. So what would we like to show here? Once we decide that we can think how to achieve it.

I was quite fond of the way it was printed at the time that I landed the patch:

    • Type indexes must match class instance head
      Expected: T (Maybe a1) <tv>
        Actual: T (Maybe a) b

That is, using tidying to emphasize the difference between the two as.

Unfortunately, I didn't notice that your commit had changed this until I validated the whole set of patches I was about to commit, at which point I just accepted the new output and moved on. (Upon further thought, I realized the new output was rather smelly, which is why I reopened this ticket.)

I'm quite keen on using "_" for the bits that don't matter

Sure. I have no preference as to whether we display other type variables as _, <tv>, or something else.

but if needs must, instead of printing (F t1 t2 t3) with one call, we can make separate calls for t1, t2, t3 etc, and that would eliminate the need to fake-up a tyvar "_" which you'll see in the code.

I'm afraid I have no idea what you are referring to with this sentence.

comment:12 Changed 9 months ago by Simon Peyton Jones <simonpj@…>

In 5b7ca039/ghc:

Wibble to Taming the Kind Inference Monster

I had allowed rename/should_fail/T15828 (Trac #15828) to regress a bit.
The main payload of this patch is to fix that problem, at the cost of
more contortions in checkConsistentFamInst.  Oh well, at least they are
highly localised.

I also update the -ddump-types code in TcRnDriver to print out some
more expicit information about each type constructor, thus instead of

   DF{3} :: forall k. * -> k -> *

we get

   data family DF{3} :: forall k. * -> k -> *

Remember, this is debug-printing only.  This change is the reason
that so many .stderr files change.

comment:13 Changed 9 months ago by simonpj

Resolution: fixed
Status: newclosed

OK it now prints it the way you had it. Hooray.

Note: See TracTickets for help on using tickets.