[GHC] #9376: Recursive closed type families fails
#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
#9376: Recursive closed type families fails -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.2 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9376: Recursive closed type families fails -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.2 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by kosmikus): Replying to [comment:1 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9376: More informative error messages when closed type families fail to simplify -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: feature | Milestone: request | Version: 7.8.2 Priority: normal | Keywords: Component: Compiler | Architecture: Unknown/Multiple (Type checker) | Difficulty: Unknown Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * type: bug => feature request Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9376: More informative error messages when closed type families fail to simplify -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: feature | Milestone: request | Version: 7.8.2 Priority: normal | Keywords: Component: Compiler | Architecture: Unknown/Multiple (Type checker) | Difficulty: Unknown Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Is the test for rhss-unify important? How bad would it be if the compatibility check ignored the RHS? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9376: More informative error messages when closed type families fail to simplify -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: feature | Milestone: request | Version: 7.8.2 Priority: normal | Keywords: Component: Compiler | Architecture: Unknown/Multiple (Type checker) | Difficulty: Unknown Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:4 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9376: More informative error messages when closed type families fail to simplify -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: feature | Milestone: request | Version: 7.8.2 Priority: normal | Keywords: Component: Compiler | Architecture: Unknown/Multiple (Type checker) | Difficulty: Unknown Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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 = () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC