Functional dependency conflicts in givens

Consider this

{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies #-}
module FunDep where

  class C a b c | a -> b c

  instance C Int Bool Char

  f :: (C Int b c) => a -> c
  f = undefined

When doing the ambiguity check we effectively ask whether this would typecheck

  g :: (C Int b c) => a -> c
  g = f

We instantiate f's type, and try to solve from g's type signature. So we end up with

  [G] d1: C Int b c
  [W] d2: C Int beta c

Now, from the fundeps we get

Interact d1 with the instance:
  [D] b ~ Bool, [D] c ~ Char

Ineract d2 with the instance:
  [D] beta ~ Bool, [D] c ~ Char

Interact d1 with d2
  [D] beta ~ b

What is annoying is that if we unify beta := b, we can solve the [W] constraint from [G], leaving only [D] constraints which we don't even always report (see discussion on #12466 (closed)). But if, randomly, we instead unify beta := Bool, we get an insoluble constraint [W] C Int Bool c, which we report. So whether or not typechecking succeeds is rather random; very unsatisfactory.

What is really wrong? Well, that Given constraint (C Int b c) is in conflict with the top-level instance decl. Maybe we should fail if that happens? But see #12466 (closed)... and Note [Given errors] in TcErrors.

The test program in Trac #13651 (closed) is just like this, only with type functions rather than type classes.

I'm not sure what to do, but I'm leaving this ticket as a record that all is not well.

Trac metadata

Trac field	Value
Version	8.2.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture