[GHC] #11605: GHC accepts overlapping instances without pragma

[GHC]

#11605: GHC accepts overlapping instances without pragma
-------------------------------------+-------------------------------------
           Reporter:  bennofs        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1-rc2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Linux
       Architecture:  x86_64         |   Type of failure:  GHC accepts
  (amd64)                            |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code is accepted by GHC (I've tested versions 7.6.3, 7.8.4,
 7.10.2, ghc 8.0.0.20160204 (rc2) and ghc 7.11.2015121 (git commit
 28638dfe79e915f33d75a1b22c5adce9e2b62b97)), even though it obviously uses
 OverlappingInstances (yet the extension is not enabled, nor are any of the
 new overlappable/ing pragmas used).

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}

 import Data.Type.Equality
 import Data.Proxy
 import Debug.Trace

 class TypeEq a b where
   eqProofClass :: Maybe (a :~: b)

 instance TypeEq a b where
   eqProofClass = Nothing

 instance TypeEq a a where
   eqProofClass = Just Refl

 data Foo a = Foo a
 instance Eq a => Eq (Foo a) where
   Foo a1 == Foo a2 = case eqProofClass :: Maybe (a :~: Int) of
     Just Refl -> traceShow (a1 :: Int,a2) (a1 == a2)
     Nothing -> a1 == (undefined :: a)

 main :: IO ()
 main = do
   print (Foo (1 :: Int) == Foo 2)
   putStrLn "--"
   print (Foo 'a' == Foo 'b')

 {- $output
 (1,2)
 False
 --
 False
 -}

 }}}

 The example does no longer compiles if I add `TypeEq a Int` to the
 instance context, it then rightfully requests `OverlappingInstances` to be
 enabled.

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