Opened 8 months ago

Last modified 8 months ago

#9376 new feature request

More informative error messages when closed type families fail to simplify

Reported by: MikeIzbicki Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

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

Change History (6)

comment:1 follow-up: Changed 8 months ago by simonpj

Are you sure that GHC 7.8.2 compiles this (the non-recursive version)?

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}

module T9376 where
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), Ord (f 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

I get

bash$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.8.2
bash$ ghc -c T9376.hs

T9376.hs:13: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 T9376.hs:12: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

And so it should! We can't simplify OrdRec Set a b to (Ord a, Ord b) because in some call to setmap you might instantiate b to an application. The paper on closed type families elaborates.

I'm puzzled how you get the behaviour you describe.

Simon

comment:2 in reply to: ↑ 1 Changed 8 months ago by kosmikus

Replying to simonpj:

Simon, your non-recursive version says:

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

OrdRec f a (f b) = ( Ord a, Ord (f b), Ord (f b) )
OrdRec f a b = ( Ord a, Ord b )

which indeed fails, but with

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 )

it compiles. Does GHC somehow recognize that the first line is a special-case of the second?

comment:3 Changed 8 months ago by goldfire

  • Summary changed from Recursive closed type families fails to More informative error messages when closed type families fail to simplify
  • Type changed from bug to feature request

The behavior seen here is as "expected", for a sufficiently nuanced expectation. I don't see an implementation bug here.

Let's look at the two different definitions in play:

type family OrdRec1 f a b where   -- closed families do kind inference!
  OrdRec1 f a (f b) = (Ord a, Ord (f b), OrdRec1 f a b)
  OrdRec1 f a b     = (Ord a, Ord b)

type family OrdRec2 f a b where
  OrdRec2 f1 a1 (f1 b1) = (Ord a1, Ord (f1 b1))
  OrdRec2 f2 a2 b2      = (Ord a2, Ord b2)

Let's try to simplify OrdRec1 Set.Set a b, for some universally-quantified a and b. The first equation of OrdRec1 clearly doesn't apply, and the second equation doesn't clearly apply. What I mean here is that we don't know enough about b: if we later learn that b is Set.Set Int, then we really should have used the first equation. GHC will not commit to a later equation when there's a possibility of using an earlier one, if it learns more about the variables involved. So, GHC gives up and refuses to simplify.

When testing with concrete types, as you have done in GHCi, OrdRec1 works just fine, as then it can be quite sure of which equation to pick.

But how does OrdRec2 work? As kosmikus guesses, GHC notices that the two cases are, in the terminology of the paper, compatible. Specifically, GHC looks at the LHSs and finds that they unify, under the substitution [f2 |-> f1, a2 |-> a1, b2 |-> f1 b1]. Then, GHC asks: will the RHSs then become the same under that substitution? In this case, the answer is yes, so GHC marks the equations as compatible. The benefit of compatibility is that GHC then isn't so sensitive about premature commitment among compatible equations. After all, if GHC chooses the second equation, but later learns that the first should be used, it wouldn't have gotten a different answer, as long as the equations are compatible.

For better or worse, you can observe some of this reasoning in OrdRec1 if you reorder either RHS. Even though constraint tuples are considered to be order-less sets, the compatibility algorithm doesn't know this, and if one of the RHSs is reordered, the compatibility check fails and GHC becomes more careful about committing to an equation during simplification.

I'm going to leave this ticket open as a request for a better error message, as this issue comes up every so often, and I'd like not to have to answer it individually each time. I think that it should be possible to note when GHC is hesitant to commit to an equation and then suggest to a user to learn more about closed type families, with a helpful link. The error message, or perhaps a new facility in GHCI, might also point out the compatibility relationships among equations, as these relationships are sometimes key to understanding a closed type family's behavior and are sometimes non-trivial for a human to derive.

comment:4 follow-up: Changed 8 months ago by simonpj

Is the test for rhss-unify important? How bad would it be if the compatibility check ignored the RHS?

comment:5 in reply to: ↑ 4 Changed 8 months ago by goldfire

Replying to simonpj:

Is the test for rhss-unify important? How bad would it be if the compatibility check ignored the RHS?

The crux of compatibility is that the RHSs unify under the substitution. Without that check, what would compatibility mean? Or, do I misunderstand your question?

comment:6 Changed 8 months ago by rwbarton

To get the desired behavior in the original program you should help GHC out a little by factoring out the common part of the two constraints.

type OrdRec (f :: * -> *) a b = ( Ord a, Ord b, OrdRec' f a b )
type family OrdRec' (f :: * -> *) a b :: Constraint where
    OrdRec' f a (f b) = OrdRec f a b
    OrdRec' f a b = ()
Note: See TracTickets for help on using tickets.