#7393: GHC cannot solve functional dependency
---------------------------------------+------------------------------------
 Reporter:  Khudyakov                  |          Owner:                  
     Type:  bug                        |         Status:  new             
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.6.1                      |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------
 GHC fails to compile following program:

 {{{
 {-# LANGUAGE MultiParamTypeClasses  #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE UndecidableInstances   #-}
 {-# LANGUAGE TypeOperators          #-}
 {-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE KindSignatures         #-}


 -- | All unordered pairs of elements of lists. If list is set result
 -- will be set as well.
 class TyPairs (xs :: [*]) (ys :: [*]) | xs -> ys

 instance                                 TyPairs '[]      '[]
 instance TyAddPairs x (x ': xs) xs ys => TyPairs (x ': xs) ys

 -- Add all pairs for /x/ and /xs/ and that build all pairs for the
 -- remaining part of the list.
 class TyAddPairs x (xs :: [*]) (rest :: [*]) (pairs :: [*]) | x xs rest ->
 pairs

 instance TyPairs    ys rs      => TyAddPairs x '[] ys rs
 instance TyAddPairs x xs ys rs => TyAddPairs x (a ': xs) ys ((x,a) ': rs)



 data K = K
 data B = B

 type List  = '[K,B]
 type Pairs = '[(K,K), (K,B), (B,B)]

 data Row (vars :: [*]) = Row

 failure :: TyPairs List r => Row r
 failure = Row :: Row Pairs

 fine :: TyPairs List Pairs => ()
 fine = ()
 }}}

 with following error message:

 {{{
 OKA/Statistics/fail.hs:36:11:
     Could not deduce (r
                       ~ (':) * (K, K) ((':) * (K, B) ((':) * (B, B) ('[]
 *))))
     from the context (TyPairs List r)
       bound by the type signature for failure :: TyPairs List r => Row r
       at OKA/Statistics/fail.hs:35:12-34
       `r' is a rigid type variable bound by
           the type signature for failure :: TyPairs List r => Row r
           at OKA/Statistics/fail.hs:35:12
     Expected type: Row r
       Actual type: Row Pairs
     In the expression: Row :: Row Pairs
     In an equation for `failure': failure = Row :: Row Pairs
 Failed, modules loaded: none.
 }}}

 r is determined by functional dependency so it looks like bug to me.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7393>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Reply via email to