[GHC] #9432: IncoherentInstances are too restricted

[GHC]

#9432: IncoherentInstances are too restricted
-------------------------------------+-------------------------------------
        Reporter:  danilo2           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8141             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by bgamari:

@@ -5,1 +5,1 @@
- extensions.html). There is one problem though. Lets consider following
+ extensions.html). There is one problem though. Let's consider following

New description:

 Hello! The reason behind using `IncoherentInstances`is that we want GHC to
 commit to a specific instance even if after instantiation of some
 variables, other instance could be more specific
 (http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-
 extensions.html). There is one problem though. Let's consider following
 example (which could not make much sense, but shows the problem well):

 {{{#!haskell
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}

 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE IncoherentInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}

 module Main where

 import Data.Typeable

 --------------------------------------------------------------------------------
 -- Type classes
 --------------------------------------------------------------------------------

 class InferType a where
     inferType :: Proxy a -> Proxy a
     inferType = undefined

 --------------------------------------------------------------------------------
 -- Proxy datatypes
 --------------------------------------------------------------------------------

 data Id0 = Id0 deriving (Show, Typeable)
 data Id1 t1 = Id1 deriving (Show, Typeable)
 data Id2 t1 t2 = Id2 deriving (Show, Typeable)
 data Id3 t1 t2 t3 = Id3 deriving (Show, Typeable)
 data Id4 t1 t2 t3 t4 = Id4 deriving (Show, Typeable)
 data Id5 t1 t2 t3 t4 t5 = Id5 deriving (Show, Typeable)

 --------------------------------------------------------------------------------
 -- Instances
 --------------------------------------------------------------------------------

 instance InferType Int

 instance (InferType m, InferType a) => InferType (m a)
 instance (a~Id0)                    => InferType (a :: *)
 instance (a~Id1)                    => InferType (a :: * -> *)
 instance (a~Id2)                    => InferType (a :: * -> * -> *)

 --------------------------------------------------------------------------------
 -- Tests
 --------------------------------------------------------------------------------
 toProxy :: a -> Proxy a
 toProxy _ = Proxy

 --inferTypeBase :: a -> Proxy a
 inferTypeBase a = inferType $ toProxy a

 instance InferType Foo1
 instance InferType Foo2

 tm _ = 5

 data Foo1 a = Foo1 a deriving (Show, Typeable)
 data Foo2 a b = Foo2 a b deriving (Show, Typeable)

 instance Monad Id1 -- dummy instances just for tests
 instance Num Id0


 main = do
     print $ typeOf $ inferType $ toProxy $ (return (5))
     print $ typeOf $ inferType $ toProxy $ (5)
     print $ typeOf $ inferType $ toProxy $ (Foo1 (return 5))
     print $ typeOf $ inferType $ toProxy $ (Foo2 (return 5) (return 5))

     print "hello"

 ---- OUTPUT:
 --    Proxy (Id1 Id0)
 --    Proxy Id0
 --    Proxy (Foo1 (Id1 Id0))
 --    Proxy (Foo2 (Id1 Id0) (Id1 Id0))
 --    "hello"

 }}}

 The idea is very simple - replace all unknown type variables with known
 ones. It works great, but the problem appears with the function
 `inferTypeBase`. It should have type of `a -> Proxy a`, but GHC claims it
 has got `Id0 -> Proxy Id0`. It is of course caused by enabled
 `-XIncoherentInstances` flag, but I think GHC should be more liberal here.
 If it really cannot pick any instance (causing an error using only
 `OverlappingInstances`), the `IncoherentInstances` should allow it to pick
 matching one even if more specific could be available after
 instantianization. But If no error would occur while using
 `OverlappingInstances`, `IncoherentInstances` should not affect the way it
 resolves the instances. I think this would make `IncoherentInstances` much
 more useful than now. Maybe it would be good to just add some options to
 the flag?

--

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