[GHC] #15621: Error message involving type families points to wrong location
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Type.Equality type family F a f :: () f = let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool b = Refl in () }}} This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Int Actual type: F Bool :~: F Bool NB: ‘F’ is a non-injective type family • In the expression: Refl In an equation for ‘a’: a = Refl In the expression: let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool .... in () | 12 | a = Refl | ^^^^ }}} This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again. Another interesting facet of this bug is that if you comment out `a`: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Type.Equality type family F a f :: () f = let {- a :: F Int :~: F Int a = Refl -} b :: F Int :~: F Bool b = Refl in () }}} Then the error message will actually point to `b` this time: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Bool Actual type: F Bool :~: F Bool NB: ‘F’ is a non-injective type family • In the expression: Refl In an equation for ‘b’: b = Refl In the expression: let b :: F Int :~: F Bool b = Refl in () | 15 | b = Refl | ^^^^ }}} The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`. This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location: {{{ $ /opt/ghc/8.0.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Bool Actual type: F Int :~: F Int NB: ‘F’ is a type function, and may not be injective • In the expression: Refl In an equation for ‘b’: b = Refl In the expression: let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool .... in () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This started happening after commit a920404fb12fb52a59e4f728cce4d662a418c5f8 (`Fix TcSimplify.decideQuantification for kind variables`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): In particular, applying this change on top of the previous commit (d4fa088350913233520ffa7163ef188a63666262) is enough to make the bug surface: {{{#!diff diff --git a/compiler/utils/UniqDFM.hs b/compiler/utils/UniqDFM.hs index 10e8aa9..3d4b1d6 100644 --- a/compiler/utils/UniqDFM.hs +++ b/compiler/utils/UniqDFM.hs @@ -147,8 +147,13 @@ addToUDFM (UDFM m i) k v = UDFM (M.insert (getKey $ getUnique k) (TaggedVal v i) m) (i + 1) addToUDFM_Directly :: UniqDFM elt -> Unique -> elt -> UniqDFM elt -addToUDFM_Directly (UDFM m i) u v = - UDFM (M.insert (getKey u) (TaggedVal v i) m) (i + 1) +addToUDFM_Directly (UDFM m i) u v + = UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1) + where + tf (TaggedVal new_v _) (TaggedVal _ old_i) = TaggedVal new_v old_i + -- Keep the old tag, but insert the new value + -- This means that udfmToList typically returns elements + -- in the order of insertion, rather than the reverse addToUDFM_Directly_C :: (elt -> elt -> elt) -> UniqDFM elt -> Unique -> elt -> UniqDFM elt }}} Since that comment mentions that `udfmToList` now returns elements in a different order than it did previously, I wonder if there is some code which was sensitive to `udfmToList`'s order that wasn't updated properly... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): We have `Refl :: forall a. Refl a a` So from the defn of `a` we instantiate `Refl` with `a := alpha`, and get {{{ [W] c1 :: alpha ~ F Int -- Line 12 [W] c2 :: alpha ~ F Int -- Line 12 }}} Each constraint carries its birth location, which I show here. Same for `b`, instantiating `Refl` with `a := beta`: {{{ [W] c3 :: beta ~ F Int -- Line 15 [W] c4 :: beta ~ F Bool -- Line 15 }}} Then depending on the order in which we try to solve, we might do {{{ alpha := beta beta := F Bool -- solves c4 }}} Now, substituting for these unified varaiables, we get {{{ [W] c1 :: F Bool ~ F Int -- Line 12 [W] c2 :: F Bool ~ F Int -- Line 12 [W] C3 :: F Bool ~ F Int -- Line 15 }}} Since these are identical, we pick one; and alas, it is `c1`. So that's why we get a bogus message. Richard, I'd be interested in your views. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This sniffs awfully like wanteds rewriting wanteds. I don't agree with the details in comment:3. You have constraints like `alpha ~ F Int`. But `CTyEqCan` documents "rhs ... has no top-level function". So these constraints look malformed. I would expect an intervening flatten metavar, which may change what's going on here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I don't agree with the details in comment:3.
Yes, I was abbreviating! What we get is {{{ -- From 'a' [W] fsk1 ~ alpha (CTyEqCan) [W] F Int ~ fsk1 (CFunEqCan) [W] fsk1 ~ alpha (CTyEqCan) -- From 'b' [W] fsk1 ~ beta (CTyEqCan) [W] fsk2 ~ beta (CTyEqCan) [W] F Bool ~ fsk2 (CFunEqCan) }}} Then from `[W] fsk1 ~ alpha` and `[W] fsk1 ~ beta` we get `[D] alpha ~ beta`. And that leads to `alpha := beta`. The `beta := F Bool` comes during unflattening. The purpose of the Derived constraints is precisely to lead to unifications, exactly as we do here. So we probalbly don't want to stop that happening. Why do we get `fsk1 ~ alpha` rather than `alpha ~ fsk1` followed by unification? See `Note [Canonical orientation for tyvar/tyvar equality constraints]` in `TcCanonical`, and `Note [Eliminate flat-skols]` in `TcType`. I think this ticket is closely related to Trac #14185. If we put the constraints from the two definitions into separate implication constraints (with no skolems and no givens), I think the Right Thing would happen. You'll see some half written code, commented out, around `alwaysBuildImplication` in `TcUnify`. I think that'd fix this. But I didn't have time to review all the error message wibbles -- probably many are improvements. Does anyone else want to have a go? The code is there! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree that the fix for #14185 will fix this precise example, but will it fix all such examples? What if there is a `Refl :: F Int :~: F Int` and a `Refl :: F Int :~: F Bool` in the same function? Then we'd be right back here. So I think #14185 is a bit of a red herring here. (I also think that fix might not fix all cases of #14185 itself.) With the way deriveds currently work, the "wanteds don't rewrite wanteds" story applies really only to skolems (which can't be "improved" through deriveds). Here, we want it also to apply to unification variables. Yet we also want to keep the work that deriveds do in other cases. I'm out of time now, but I don't think this will be so easy, somehow... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
What if there is a Refl :: F Int :~: F Int and a Refl :: F Int :~: F Bool in the same function?
It's fine. Each type signature will give rise to its own implication constraint (indeed already does, except that it is optimised away for signatures that are monotypes). So I think that #14185 is not a red herring at all! I agree that there is a tension here. The ''whole point'' of Deriveds, the only reason they exist, is so that we can more vigorously rewrite wanteds with wanteds, and thus find equalities that must hold in any ultimate solution. The trouble is that there may still be a choice of which unifications to do in which order, and that affects error messages. I'm proposing our implication constraints as a way to keep the two sub- problems separate. (They won't ''stay'' separate, because we'll float out any unsolved equality constraints - and indeed deliberately so, so that they can meet friends from other equality constraints and we can learn more equalities thereby. But they will at least ''begin'' separate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But what about a function that mentions {{{#!hs let x = (Refl :: F Int :~: F Int) `seq` (Refl :: F Int :~: F Bool) `seq` () }}} We'll get the error on the wrong line, won't we? The solution to #14185 improves the status quo, but only by a lucky coincidence (that the problems in both tickets stem from two different functions). What's nice about #14185 is that it prevents the error from jumping arbitrarily far in a file, but I still don't think it's the real solution to the problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
The solution to #14185 improves the status quo, but only by a lucky coincidence (that the problems in both tickets stem from two different functions)
NO, as I say in comment:7, each type signature makes a new implication constraint, so that'll keep their constraints separate. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: 8.6.1 => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15621: Error message involving type families points to wrong location -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.4.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by pacak): One more example, figuring out why ghc complains on an innocent looking line took a bit of time. {{{ % cat foo.hs }}} {{{#!haskell module P (o_O) where import GHC.Types o_O :: Maybe Any o_O = do present <- pure True if present then undefined :: Maybe Int else undefined :: Maybe Int }}} {{{ % ghc -O foo.hs [1 of 1] Compiling P ( foo.hs, foo.o ) foo.hs:7:5: error: • Couldn't match type ‘Any’ with ‘Int’ Expected type: Maybe Any Actual type: Maybe Int • In a stmt of a 'do' block: present <- pure True In the expression: do present <- pure True if present then undefined :: Maybe Int else undefined :: Maybe Int In an equation for ‘o_O’: o_O = do present <- pure True if present then undefined :: Maybe Int else undefined :: Maybe Int | 7 | present <- pure True | ^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15621#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC