Opened 7 months ago

Last modified 4 months ago

#9432 new bug

IncoherentInstances are too restricted

Reported by: danilo2 Owned by:
Priority: high Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #8141 Differential Revisions:

Description (last modified by danilo2)

Hello! The reason behind using IncoherentInstancesis 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):

{-# 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?

Change History (4)

comment:1 Changed 7 months ago by danilo2

Maybe we should treat it as a bug? I've got here a small example showing that it really breaks how OverlappingInstances are working:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE IncoherentInstances #-} -- the flag is niot needed by the example

module Main where
import Data.Typeable


class CTest a b | a -> b where
    cTest :: a -> b

-- this instance is choosen even if more specific is available!
instance out~a => CTest a out where
    cTest = id

instance CTest Int String where
    cTest _ = "test"


main = do
    print $ typeOf $ cTest (5::Int)

The instance CTest a out even if more specific (CTest Int String) is in scope, which just breaks how OverlappingInstances work. If we disable the IncoherentInstances flag, the right one is selected.

Last edited 7 months ago by danilo2 (previous) (diff)

comment:2 Changed 7 months ago by danilo2

  • Type changed from feature request to bug

comment:3 Changed 7 months ago by danilo2

  • Description modified (diff)

comment:4 Changed 4 months ago by thomie

Note: See TracTickets for help on using tickets.