[GHC] #15361: Error message displays redundant equality constraint
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: #14394 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When compiling this program: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality foo :: forall (a :: Type) (b :: Type) (c :: Type). a :~~: b -> a :~~: c foo HRefl = HRefl }}} GHC complains thus: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12:13: error: • Could not deduce: a ~ c from the context: (* ~ *, b ~ a) bound by a pattern with constructor: HRefl :: forall k1 (a :: k1). a :~~: a, in an equation for ‘foo’ at Bug.hs:12:5-9 ‘a’ is a rigid type variable bound by the type signature for: foo :: forall a b c. (a :~~: b) -> a :~~: c at Bug.hs:(10,1)-(11,27) ‘c’ is a rigid type variable bound by the type signature for: foo :: forall a b c. (a :~~: b) -> a :~~: c at Bug.hs:(10,1)-(11,27) Expected type: a :~~: c Actual type: a :~~: a • In the expression: HRefl In an equation for ‘foo’: foo HRefl = HRefl • Relevant bindings include foo :: (a :~~: b) -> a :~~: c (bound at Bug.hs:12:1) | 12 | foo HRefl = HRefl | ^^^^^ }}} That `* ~ *` constraint is entirely redundant. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But you put it there, by matching on heterogeneous equality on types all of kind `Type`. Do you propose that GHC not mention givens that are implied by other givens? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:1 goldfire]:
Do you propose that GHC not mention givens that are implied by other givens?
Certainly not, and moreover, GHC already does not mention redundant implied givens in certain situations. In this code: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} import Data.Type.Equality data Goo a where MkGoo :: (Ord a, a ~ Bool) => a -> Goo a goo :: Goo a -> a :~: b goo MkGoo{} = Refl }}} {{{ Bug.hs:10:15: error: • Could not deduce: b ~ Bool from the context: (Ord a, a ~ Bool) bound by a pattern with constructor: MkGoo :: forall a. (Ord a, a ~ Bool) => a -> Goo a, in an equation for ‘goo’ at Bug.hs:10:5-11 ‘b’ is a rigid type variable bound by the type signature for: goo :: forall a b. Goo a -> a :~: b at Bug.hs:9:1-23 Expected type: a :~: b Actual type: a :~: a • In the expression: Refl In an equation for ‘goo’: goo MkGoo {} = Refl • Relevant bindings include goo :: Goo a -> a :~: b (bound at Bug.hs:10:1) | 10 | goo MkGoo{} = Refl | ^^^^ }}} GHC does not bother warning about an `Eq a` constraint being in the context bound by the `MkGoo` pattern match, even though it is implied by `Ord a`. Moreover, in this code: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} import Data.Type.Equality hoo :: Int :~: Int -> a :~: b -> a :~: c hoo Refl Refl = Refl }}} {{{ Bug.hs:7:17: error: • Could not deduce: a ~ c from the context: b ~ a bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for ‘hoo’ at Bug.hs:7:10-13 ‘a’ is a rigid type variable bound by the type signature for: hoo :: forall a b c. (Int :~: Int) -> (a :~: b) -> a :~: c at Bug.hs:6:1-40 ‘c’ is a rigid type variable bound by the type signature for: hoo :: forall a b c. (Int :~: Int) -> (a :~: b) -> a :~: c at Bug.hs:6:1-40 Expected type: a :~: c Actual type: a :~: a • In the expression: Refl In an equation for ‘hoo’: hoo Refl Refl = Refl • Relevant bindings include hoo :: (Int :~: Int) -> (a :~: b) -> a :~: c (bound at Bug.hs:7:1) | 7 | hoo Refl Refl = Refl | ^^^^ }}} GHC does not warn about an `Int ~ Int` constraint, even though we "put it there" by matching on a value of type `Int :~: Int`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I find the second example more convincing than the first. I wonder how we do that... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): We can fix this issue with the following patch: {{{#!diff diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 95dc152..1098b1f 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -1821,7 +1821,7 @@ pp_givens givens where ppr_given herald (Implic { ic_given = gs, ic_info = skol_info , ic_env = env }) - = hang (herald <+> pprEvVarTheta gs) + = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs)) 2 (sep [ text "bound by" <+> ppr skol_info , text "at" <+> ppr (tcl_loc env) ]) }}} (Where `pp_givens` is the function that prints out the stuff after `from the context:`.) Does this sound like a reasonable approach? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Well, if it's that easy, yes, I'm quite happy with it. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5002 Comment: In that case, I'll go for that approach. See Phab:D5002. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I was puzzled about why redundant givens are sometimes reported and sometimes not. Here's the deal * For each implication GHC figures out, during constraint solving, whether the implication binds any equalities. This is used to guide equality float-out, and is recorded in the implication in the `ic_no_eqs` field. * The "whether binds any equalities" test is performed on the ''canonicalised, inert givens'', in `TcSMonad.getNoGivenEqs`. See `Note [When does an implication have given equalities?]`. * If an implication binds `* ~ *` only (call it situation (A)), we'll discard that Given, and mark the implication as `ic_no_eqs = True`. * But if an implication binds `* ~ *` ''and'' `a ~ b`, situation (B), the `ic_no_eqs` field will be set `False`. * When reporting an equality error, we report givens only from implications with `ic_no_eqs` = `False`. That makes sense. But it'll discard situation (A), and keep situation (B). * For the implications we keep, we report all original, user-written givens. Hence the reported `* ~ *`. So that explain the behavior you see. For example for `hoo` in comment:2, the `Int :~: Int` binds no equalities because when `Int ~ Int` is solved we get nothing. So it is not reported. I suppose, therefore, that the solution you suggest is no unreasonable, ''provided'' you write Note to explain. In particular * `mkMinimalBySCs` happens to eliminate reflexive equalities, as well as superclasses. (Why? See Note [Remove redundant provided dicts]` in `TcPatSyn`. * Explain how a given `* ~ *` can arise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:7 simonpj]:
I suppose, therefore, that the solution you suggest is no unreasonable, ''provided'' you write Note to explain.
Sure thing. I've updated Phab:D5002. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler (Type | Version: 8.4.3
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Poor/confusing | Unknown/Multiple
error message | Test Case:
Blocked By: | Blocking:
Related Tickets: #14394 | Differential Rev(s): Phab:D5002
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: 8.8.1 => 8.6.1 Comment: This was marked as merge, but not milestoned properly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15361: Error message displays redundant equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: #14394 | Differential Rev(s): Phab:D5002 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged in 89ad5fed345d54ed73ecb3057346f3ef81864c8c. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC