[GHC] #9376: Recursive closed type families fails

29 Jul 2014

      #9376: Recursive closed type families fails
-------------------------------------+-------------------------------------
       Reporter:  MikeIzbicki        |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.2
  checker)                           |        Operating System:
       Keywords:                     |  Unknown/Multiple
   Architecture:  Unknown/Multiple   |         Type of failure:
     Difficulty:  Unknown            |  None/Unknown
     Blocked By:                     |               Test Case:
Related Tickets:                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 In the following code, I am getting strange compiler errors that I suspect
 has to do with the recursive application of the OrdRec type family:

 {{{
 import GHC.Prim
 import Data.Proxy
 import qualified Data.Set as Set

 type family OrdRec (f :: * -> *) a b  :: Constraint where
     OrdRec f a (f b) = ( Ord a, Ord (f b), OrdRec f a b )
     OrdRec f a b = ( Ord a, Ord b )

 setmap :: OrdRec Set.Set a b => (a -> b) -> Set.Set a -> Set.Set b
 setmap f set = Set.map f set
 }}}

 GHC gives the error message:

 {{{
 ClosedTypeFamilyRecursion.hs:11:16:
     Could not deduce (Ord b) arising from a use of ‘Set.map’
     from the context (OrdRec Set.Set a b)
       bound by the type signature for
                  setmap :: (OrdRec Set.Set a b) =>
                            (a -> b) -> Set.Set a -> Set.Set b
       at ClosedTypeFamilyRecursion.hs:10:11-66
     Possible fix:
       add (Ord b) to the context of
         the type signature for
           setmap :: (OrdRec Set.Set a b) =>
                     (a -> b) -> Set.Set a -> Set.Set b
     In the expression: Set.map f set
     In an equation for ‘setmap’: setmap f set = Set.map f set
 Failed, modules loaded: none.
 }}}

 If we modify the OrdRec type family to remove the recursive application:

 {{{
 type family OrdRec (f :: * -> *) a b  :: Constraint where
     OrdRec f a (f b) = ( Ord a, Ord (f b) )
     OrdRec f a b = ( Ord a, Ord b )
 }}}

 Then GHC is able to compile the file fine.

 What's extra weird, though, is that ghci appears to be able to evaluate
 the recursive type family correctly.  If we comment out the setmap
 function, then load into ghci, we can verify that the OrdRec type family
 is giving the correct Ord constraints:

 {{{
 ghci> :t Proxy :: Proxy (OrdRec [] Int Float)
 Proxy :: Proxy (OrdRec [] Int Float) :: Proxy (Ord Int, Ord Float)

 ghci> :t :t Proxy :: Proxy (OrdRec [] Int [Float])
 Proxy :: Proxy (OrdRec [] Int [Float])
   :: Proxy (Ord Int, Ord [Float], (Ord Int, Ord Float))

 ghci> :t Proxy :: Proxy (OrdRec [] Int [[Float]])
 Proxy :: Proxy (OrdRec [] Int [[Float]])
   :: Proxy
        (Ord Int,
         Ord [[Float]],
         (Ord Int, Ord [Float], (Ord Int, Ord Float)))
 }}}

 But if I try to define the setmap function interactively in ghci, I get
 the same error message:

 {{{
 ghci> > let setmap = (\f set -> Set.map f set) :: OrdRec Set.Set a b => (a
 -> b) -> Set.Set a -> Set.Set b

 <interactive>:39:25:
     Could not deduce (Ord b1) arising from a use of ‘Set.map’
     from the context (OrdRec Set.Set a b)
       bound by the inferred type of
                setmap :: (OrdRec Set.Set a b) =>
                          (a -> b) -> Set.Set a -> Set.Set b
       at <interactive>:39:5-98
     or from (OrdRec Set.Set a1 b1)
       bound by an expression type signature:
                  (OrdRec Set.Set a1 b1) => (a1 -> b1) -> Set.Set a1 ->
 Set.Set b1
       at <interactive>:39:14-98
     Possible fix:
       add (Ord b1) to the context of
         an expression type signature:
           (OrdRec Set.Set a1 b1) => (a1 -> b1) -> Set.Set a1 -> Set.Set b1
         or the inferred type of
            setmap :: (OrdRec Set.Set a b) =>
                      (a -> b) -> Set.Set a -> Set.Set b
     In the expression: Set.map f set
     In the expression:
         (\ f set -> Set.map f set) ::
           OrdRec Set.Set a b => (a -> b) -> Set.Set a -> Set.Set b
     In an equation for ‘setmap’:
         setmap
           = (\ f set -> Set.map f set) ::
               OrdRec Set.Set a b => (a -> b) -> Set.Set a -> Set.Set b
 }}}

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