[GHC] #12647: Can't capture improvement of functional dependencies

30 Sep 2016

      #12647: Can't capture improvement of functional dependencies
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  None           |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  FunctionalDependencies             |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 [http://www.diku.dk/~paba/pubs/files/serrano15haskell-paper.pdf Type
 Families with Class, Type Classes with Family] discusses
 [https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdf-
 instance-improvement instance improvement] with the example

 {{{#!hs
 class Collection c e | c -> e where
   empty :: c
   add   :: e -> c -> c

 instance Collection [a] a where
   empty :: [a]
   empty = []

   add :: a -> [a] -> [a]
   add = (:)
 }}}

 I wondered how to express that `x ~ Int` can be deduced from `Collection
 [Int] x` using improvement, I first attempted using the
 [https://hackage.haskell.org/package/constraints constraints] machinery:

 {{{#!hs
 data Dict c where
   Dict :: c => Dict c

 newtype a :- b = Sub (a => Dict b)
 }}}

 but I'm not able to construct a term of type `Collection [Int] x :- (Int ~
 x)` proving that `Collection [Int] x` entails `Int ~ x`:

 {{{
 ghci> Sub Dict :: Collection [Int] x :- (Int ~ x)

 <interactive>:52:5: error:
     • Couldn't match type ‘x1’ with ‘Int’ arising from a use of ‘Dict’
       ‘x1’ is a rigid type variable bound by
         an expression type signature:
           forall x1. Collection [Int] x1 :- Int ~ x1
         at <interactive>:52:13
     • In the first argument of ‘Sub’, namely ‘Dict’
       In the expression: Sub Dict :: Collection [Int] x :- (Int ~ x)
       In an equation for ‘it’:
           it = Sub Dict :: Collection [Int] x :- (Int ~ x)
 }}}

 Is this due to overlapping instances or something?

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