[GHC] #9432: IncoherentInstances are too restricted

[GHC]

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

Old 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.0.4/html/users_guide/type-class-
> extensions.html). There is one problem though. Lets 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?

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. Lets 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:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler