[GHC] #14745: Functional dependency conflicts in givens

31 Jan 2018

      #14745: Functional dependency conflicts in givens
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14745
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler