GitLab

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