[GHC] #8155: Defaulting bug or unfortunate error message with closed type families
#8155: Defaulting bug or unfortunate error message with closed type families ------------------------------------+------------------------------------- Reporter: nh2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- https://github.com/nh2/infinite-type-families/blob/master/Test2.hs Some code extracted from hmatrix: {{{ {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} module Test where data Vector a = Vector a data Matrix a = Matrix a class Build f where build' :: BoundsOf f -> f -> ContainerOf f #if __GLASGOW_HASKELL__ <= 706 -- Normal type families with GHC 7.6, works well. type family BoundsOf x type instance BoundsOf (a->a) = Int type instance BoundsOf (a->a->a) = (Int,Int) type family ContainerOf x type instance ContainerOf (a->a) = Vector a type instance ContainerOf (a->a->a) = Matrix a #else -- Closed type families for GHC 7.8 type family BoundsOf x where BoundsOf (a->a->a) = (Int,Int) BoundsOf (a->a) = Int type family ContainerOf x where ContainerOf (a->a) = Vector a ContainerOf (a->a->a) = Matrix a #endif instance (Num a) => Build (a->a) where build' = buildV buildV :: (Integral a, Num b) => a -> (b -> c) -> Vector c buildV _ _ = undefined }}} This is probably related to #8154. With GHC 7.7, we get the following error: {{{ Test2.hs:59:14: Could not deduce (BoundsOf (a -> a) ~ Integer) from the context (Num a) bound by the instance declaration at Test2.hs:58:10-32 Expected type: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) Actual type: Integer -> (a -> a) -> Vector a Relevant bindings include build' :: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) (bound at Test2.hs:59:5) In the expression: buildV In an equation for ‛build'’: build' = buildV }}} 1) Where does this Integer come from? 2) Change {{{ BoundsOf (a->a) = Int }}} into {{{ BoundsOf (a->a) = Integer }}} You get the same error message, although clearly {{{BoundsOf (a -> a) ~ Integer}}} (you just wrote that down).[[BR]] Even if the order matters in closed type families, is this not the wrong error message? 3) If you flip the order so that the (a->a) case comes first, it works (with both it Int or Integer). I don't quite understand why. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8155: Defaulting bug or unfortunate error message with closed type families -------------------------------------+------------------------------------ Reporter: nh2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: This may be an infelicity in defaulting (which I'm not terribly familiar with), but the closed-type-family behavior is correct, if rather subtle and confusing. The original post says "clearly `BoundsOf (a -> a) ~ Integer` (you just wrote that down)". I would say that that's not exactly what was written. What the closed-type-family definition of `BoundsOf` says is that `BoundsOf (a -> a) ~ Integer` as long as `a` is most assuredly '''not''' `a -> a`. That is, GHC must be sure that previous equations of a closed type family can never apply before using a given equation. Because it is quite possible that `a` will be instantiated at a type such that `a` '''does''' equal `a -> a` (see below), GHC will not use the second equation to simplify `BoundsOf (a -> a)`. The dangerous type that `a` might be instantiated with is {{{ type family Looper b type instance Looper b = Looper b -> Looper b }}} So, unless GHC knows that `a` won't be instantiated at a type like `Looper`, the second equation will not be used. As a concrete example of this, GHC will happily reduce `BoundsOf (Bool -> Bool)`. This is all very subtle and can be unexpected, but after lots and lots of thinking, Simon PJ, Dimitrios V, and I could not come up with a better way here. When I wrote a suggested implementation of `BoundsOf` in my response to #8154, I thought a little while about the ordering of the equations to avoid exactly this problem. I will close this ticket, but do please reopen if you can characterize the bug as a specific infelicity in the defaulting mechanism. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
This may be an infelicity in defaulting (which I'm not terribly familiar with)
[...]
I will close this ticket, but do please reopen if you can characterize
#8155: Defaulting bug or unfortunate error message with closed type families -------------------------------------+------------------------------------ Reporter: nh2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by nh2): Replying to [comment:1 goldfire]: the bug as a specific infelicity in the defaulting mechanism. I know too little about how defaulting works, we would need somebody who understands that.
This is all very subtle and can be unexpected, but after lots and lots of thinking, Simon PJ, Dimitrios V, and I could not come up with a better way here
I am not saying that I find this behaviour of closed type families wrong or so. Is it not possible to change the generated error message to give a hint why this is rejected, e.g. based on what you explained here? I understand your reasoning here, but had I not seen your example here and would I encounter this message in GHC with the current error message, chances are high I'd think it's a bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8155: Defaulting bug or unfortunate error message with closed type families -------------------------------------+------------------------------------ Reporter: nh2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): It's hard for me to see how to do this. It seems that the problem is that your closed type family contains an equation which does not fire in the general case. But, this equation does fire in more specific cases, when the type variable is fully instantiated. I could imagine issuing a warning in this situation, but it would seem that this isn't always a programmer mistake. I could also imagine tracking when you have an equation like this that doesn't fire and then reporting that to the user along with other type errors, in case those errors are related. But, that would take a fair amount of very specific plumbing to pull together, and it's not obvious that this is the right idea. Do you see a better way forward here? What should be reported and when? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8155: Defaulting bug or unfortunate error message with closed type families
-------------------------------------+------------------------------------
Reporter: nh2 | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
Resolution: invalid | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Simon Peyton Jones
#8155: Defaulting bug or unfortunate error message with closed type families
-------------------------------------+------------------------------------
Reporter: nh2 | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
Resolution: invalid | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Simon Peyton Jones
#8155: Defaulting bug or unfortunate error message with closed type families -------------------------------------+------------------------------------ Reporter: nh2 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * status: closed => new * resolution: invalid => Comment: Thank you for identifying this problem. Once I understood it, the fix was easy. New error message is much more sensible {{{ T8155.hs:26:14: Could not deduce (Integral (BoundsOf (a -> a))) arising from a use of ‛buildV’ from the context (Num a) bound by the instance declaration at T8155.hs:25:10-32 In the expression: buildV In an equation for ‛build'’: build' = buildV In the instance declaration for ‛Build (a -> a)’ }}} Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8155: Defaulting bug or unfortunate error message with closed type families -------------------------------------------------+------------------------- Reporter: nh2 | Owner: Type: bug | Status: Priority: normal | closed Component: Compiler | Milestone: Resolution: fixed | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple indexed_types/should_fail/T8155 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed_types/should_fail/T8155 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8155#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8155: Defaulting bug or unfortunate error message with closed type families
--------------------------+------------------------------------------------
Reporter: nh2 | Owner:
Type: bug | Status: closed
Priority: | Milestone:
normal |
Component: | Version: 7.6.3
Compiler |
Resolution: fixed | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple |
Type of failure: | Test Case: indexed_types/should_fail/T8155
None/Unknown |
Blocked By: | Blocking:
Related Tickets: |
--------------------------+------------------------------------------------
Comment (by Simon Peyton Jones
participants (1)
-
GHC