[GHC] #12538: Incorrect uses of overlapping instances and data families sends GHC into loop

[GHC]

#12538: Incorrect uses of overlapping instances and data families sends GHC into
loop
-------------------------------------+-------------------------------------
           Reporter:  pkmx           |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Sorry for the lack of descriptive title, as I can't nail down the source
 of this specific bug. This is the minimal example to trigger the loop:

 {{{#!hs
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}

 module Main where

 import GHC.TypeLits
 import GHC.Types

 data Tagged t a = Tagged a

 type family Tag a where
   Tag (Tagged t a) = Tagged t a
   Tag a = Tagged Int a

 class (r ~ Tag a) => TagImpl a r | a -> r where
   tag :: a -> r

 instance {-# OVERLAPPING #-} (r ~ Tag (Tagged t a)) => TagImpl (Tagged t
 a) r where
   tag = id

 #ifdef WRONG
 instance {-# OVERLAPPING #-} (r ~ Tagged t a, r ~ Tag a) => TagImpl a r
 where
 #else
 instance {-# OVERLAPPING #-} (r ~ Tagged Int a, r ~ Tag a) => TagImpl a r
 where
 #endif
   tag = Tagged @Int

 data family   DF x
 data instance DF (Tagged t a) = DF (Tagged t a)

 class ToDF a b | a -> b where
   df :: a -> b

 #ifdef WRONG
 instance (TagImpl a a', b ~ DF a') => ToDF a b where
 #else
 instance (TagImpl a (Tagged t a'), b ~ DF (Tagged t a')) => ToDF a b where
 #endif
   df = DF . tag

 main :: IO ()
 main = pure ()
 }}}

 When compiled with `-DWRONG`, it causes GHC (both 8.0.1 and HEAD at 20160823)
 to loop:

 {{{
 $ ghc --version && ghc -fno-code Main.hs -DWRONG
 The Glorious Glasgow Haskell Compilation System, version 8.1.20160823
 [1 of 1] Compiling Main             ( Main.hs, nothing )
 (loops indefinitely...)
 }}}

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