Opened 15 months ago
Last modified 15 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 Rev(s): | ||
Wiki Page: |
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: ↓ 2 Changed 15 months ago by simonpj
comment:2 in reply to: ↑ 1 Changed 15 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 15 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: ↓ 5 Changed 15 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 15 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 15 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 = ()
Are you sure that GHC 7.8.2 compiles this (the non-recursive version)?
I get
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