[GHC] #16002: Type family equation with wrong name is silently accepted (GHC 8.6+ only)

5 Dec 2018

      #16002: Type family equation with wrong name is silently accepted (GHC 8.6+ only)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.6.2
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's a program:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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
   |   ^^^^^^^
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16002
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler