Opened 10 months ago

Closed 9 months ago

#16002 closed bug (fixed)

Type family equation with wrong name is silently accepted (GHC 8.6+ only)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.6.2
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: rename/should_fail/T16002
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5420
Wiki Page:

Description

Here's a program:

{-# LANGUAGE TypeFamilies #-}
module TypeFamilies where

data A
type family B (x :: *) :: * where
  A x = x

One would hope that GHC would reject that nonsensical equation for B that references A. On GHC 7.8 through 8.4, that is the case:

$ /opt/ghc/8.4.4/bin/ghci Bug.hs
GHCi, version 8.4.4: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling TypeFamilies     ( Bug.hs, interpreted )

Bug.hs:6:3: error:
    • Mismatched type name in type family instance.
        Expected: B
          Actual: A
    • In the type family declaration for ‘B’
  |
6 |   A x = x
  |   ^^^^^^^

But GHC 8.6.2 and HEAD actually accept this program! Thankfully, GHC appears to just treat A x = x as though you had written B x = x, so it's not like this breaks type safety or anything. Still, this most definitely ought to be rejected.

One interesting observation is that B having a CUSK appears to be important. If B doesn't have a CUSK, as in the following variant:

{-# LANGUAGE TypeFamilies #-}
module TypeFamilies where

data A
type family B x where
  A x = x

Then GHC properly catches the mismatched use of A:

$ /opt/ghc/8.6.2/bin/ghci Bug.hs
GHCi, version 8.6.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling TypeFamilies     ( Bug.hs, interpreted )

Bug.hs:6:3: error:
    • Mismatched type name in type family instance.
        Expected: B
          Actual: A
    • In the type family declaration for ‘B’
  |
6 |   A x = x
  |   ^^^^^^^

Change History (8)

comment:1 Changed 10 months ago by RyanGlScott

This regression was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.).

comment:2 Changed 10 months ago by RyanGlScott

Ah, it's due to this change:

 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
   -- See Note [Kind checking for type and class decls]
 kcLTyClDecl (L loc decl)
+  | hsDeclHasCusk decl
+  = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
+  | otherwise
   = setSrcSpan loc $
     tcAddDeclCtxt decl $
-    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
+    do { traceTc "kcTyClDecl {" (ppr tc_name)
        ; kcTyClDecl decl
-       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }
+       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
+  where
+    tc_name = tyClDeclLName decl

Note that kcTyClDecl (which performs the validity check needed to reject A x = x above) is only invoked when a type family declaration lacks a CUSK!

NB: This code no longer exists in GHC HEAD, as it has since been refactored into kcTyClGroup:

kcTyClGroup decls
  = do  { ...

        ; let (cusk_decls, no_cusk_decls)
                 = partition (hsDeclHasCusk . unLoc) decls

        ; ...

        ; mapM_ kcLTyClDecl no_cusk_decls

        ; ... }

comment:3 Changed 10 months ago by RyanGlScott

(Interestingly, this exact bit of code was also responsible for causing #15116.)

comment:4 Changed 10 months ago by simonpj

Ah yes, good catch. I think the Right Thing is to move the test out of kcTyFamInstEqn and put it in RnSource.rnFamInstEqn. That way it'll be nailed by the renamer, which has plenty of information to give a good error message.

Would you consider doing that?

comment:5 Changed 10 months ago by RyanGlScott

Differential Rev(s): Phab:D5420
Status: newpatch

Moving the check to the renamer seems to work pretty well!

comment:6 Changed 10 months ago by carter

should this fix go into a 8.6.3?

Last edited 10 months ago by carter (previous) (diff)

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

In 28f41f1a/ghc:

Fix #16002 by moving a validity check to the renamer

Summary:
The validity check which rejected things like:

```lang=haskell
type family B x where
  A x = x
```

Used to live in the typechecker. But it turns out that this validity
check was //only// being run on closed type families without CUSKs!
This meant that GHC would silently accept something like this:

```lang=haskell
type family B (x :: *) :: * where
  A x = x
```

This patch fixes the issue by moving this validity check to the
renamer, where we can be sure that the check will //always// be run.

Test Plan: make test TEST=T16002

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: goldfire, rwbarton, carter

GHC Trac Issues: #16002

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

comment:8 Changed 9 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: rename/should_fail/T16002
Note: See TracTickets for help on using tickets.