Opened 3 years ago

Last modified 3 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 Rev(s):
Wiki Page:

Description (last modified by bgamari)

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 ( There is one problem though. Let's 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 (8)

comment:1 Changed 3 years 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 3 years ago by danilo2 (previous) (diff)

comment:2 Changed 3 years ago by danilo2

Type: feature requestbug

comment:3 Changed 3 years ago by danilo2

Description: modified (diff)

comment:4 Changed 3 years ago by thomie

comment:5 Changed 4 months ago by diatchki

I am not sure I understand the issue here, could you provide an example using the new notation for incoherent and overlapping instances (i.e., where each instance is annotated individually, rather than having the global flag).

comment:6 Changed 4 months ago by rwbarton

These two issues seem unrelated (the second one has something to do with functional dependencies) and should probably be in two separate tickets.

comment:7 Changed 3 months ago by bgamari

Description: modified (diff)

comment:8 Changed 3 months ago by simonpj

Yes these are two distinct issues. I've made #13284 for comment:1.

I don't really understand the problem in the Description. Does it not suffice to add the signature

inferTypeBase :: InferType a => a -> Proxy a
Note: See TracTickets for help on using tickets.