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 |