Opened 22 months ago

Last modified 22 months ago

#14745 new bug

Functional dependency conflicts in givens

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: FunDeps Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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). 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... and Note [Given errors] in TcErrors.

The test program in Trac #13651 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.

Change History (2)

comment:1 Changed 22 months ago by simonpj

Keywords: FunDeps added

comment:2 Changed 22 months ago by Simon Peyton Jones <simonpj@…>

In efba0546/ghc:

Prioritise equalities when solving, incl deriveds

We already prioritise equalities when solving, but
Trac #14723 showed that we were not doing so consistently
enough, and as a result the type checker could go into a loop.
Yikes.

See Note [Prioritise equalities] in TcSMonad.

Fixng this bug changed the solve order enough to demonstrate
a problem with fundeps: Trac #14745.
Note: See TracTickets for help on using tickets.