GitLab

EDIT: The ticket was original discovered in the context of the ambiguity checker, and it took some time to figure out that this has nothing to do with ambiguity: it's just about non-confluence in the constraint solver. See helpful examples in #17295 (comment 226331) and #17295 (comment 237871)

The ambiguity checker seems to be doing strange things in the presence of quantified constraints. In particular, you can cause it to try and start solving for arbitrary equalities, which I find strange. And it won't listen to AllowAmbiguousTypes.

[edit @Ericson2314 comment with smaller example: #17295 (comment 231973)]

Here's a minimized example:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-} -- This fails with and without AllowAmbiguousTypes...

data A
data B

foo :: (A ~ B => a ~ A) => (a ~ A => ()) -> ()
foo _ = ()

GHC reports:

 error:
    • Couldn't match type ‘A’ with ‘B’
    • In the ambiguity check for ‘foo’
      In the type signature:
        foo :: (A ~ B => a ~ A) => (a ~ A => ()) -> ()

I haven't been able to provoke this behaviour without quantified constraints.

I've tested the above with GHC 8.8.1, though it's also likely broken on HEAD too.