Overlapping instances mentioning constructor-bound type variables give no error
Summary
Constraints mentioning type variable bound by data constructor are solved even when they trigger overlapping instances.
Steps to reproduce
{-# LANGUAGE FlexibleInstances, ExistentialQuantification #-}
module Bug where
import Data.Proxy
class Foo x where
x :: Proxy x -> String
instance Foo Int where
x _ = "Int"
instance Foo a where
x _ = "-"
data SomeProxy = forall x . SomeProxy (Proxy x)
foo :: SomeProxy -> String
foo (SomeProxy p) = x p
This code compiles without an error, although Foo Int
and Foo a
are obviously overlapping. Encoding existential type via universal quantification fails as expected
bar :: ((forall x . Proxy x -> String) -> String) -> String
bar f = f x
• Overlapping instances for Foo x arising from a use of ‘x’
Matching instances:
instance Foo a -- Defined at Bug.hs:15:10
instance Foo Int -- Defined at Bug.hs:12:10
(The choice depends on the instantiation of ‘x’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
Expected behavior
Compiling foo
gives the same error as bar
.
Environment
- GHC version used: 8.10.4, 9.0.1, 9.3.20210504
- Operating System: Linux (NixOS)
- System Architecture: x86-64