[GHC] #10789: Notify user when a kind mismatch holds up a type family reduction
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- Consider this contrived example: {{{ {-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances #-} module Bug where import Data.Proxy type family F (a :: k) :: k type instance F a = G a type family G a type instance G a = a foo :: Proxy (F Maybe) -> Proxy Maybe foo = id }}} This (correctly) fails to compile. The error message is {{{ Bug.hs:14:7: Couldn't match type ‘F Maybe’ with ‘Maybe’ Expected type: Proxy (F Maybe) -> Proxy Maybe Actual type: Proxy Maybe -> Proxy Maybe In the expression: id In an equation for ‘foo’: foo = id Failed, modules loaded: none. }}} But this is peculiar, but it surely looks like `F` should be a type-level identity function! Of course, upon further inspection, we see that `F` is partial. It reduces only at kind `*`. This is quite hard to figure out, though, especially given that we're using the "default to `*`" behavior of open type families to arrange for this kind restriction. Thus, I propose: figure out when a type family reduction is held up due to a kind mismatch, and inform the user. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): See also #10775 for the error that originally inspired this request. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => newcomer * milestone: => 7.12.1 Comment: A little coding in `TcErrors` should do it. Happy to advise someone who wants to take this on. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ssequeira Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ssequeira): * owner: => ssequeira * milestone: 8.0.1 => ⊥ -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ssequeira Type: feature request | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * milestone: ⊥ => 8.0.1 Comment: Thanks, ssequeira! I assume the change in milestone was accidental, and so I'm reverting it. Setting a milestone to bottom effectively means that we've given up on the ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: ssequeira Type: feature request | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thoughtpolice): * milestone: 8.0.1 => 8.0.2 Comment: I'm bumping this to 8.0.2 and moving this from the 8.0.1 queue, since it's not critical but would be 'nice to have' for error messages. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * owner: ssequeira => Comment: Please reassign yourself ssequeira if you are still working on this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.0.2 => 8.2.1 @@ -3,1 +3,1 @@ - {{{ + {{{#!hs New description: Consider this contrived example: {{{#!hs {-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances #-} module Bug where import Data.Proxy type family F (a :: k) :: k type instance F a = G a type family G a type instance G a = a foo :: Proxy (F Maybe) -> Proxy Maybe foo = id }}} This (correctly) fails to compile. The error message is {{{ Bug.hs:14:7: Couldn't match type ‘F Maybe’ with ‘Maybe’ Expected type: Proxy (F Maybe) -> Proxy Maybe Actual type: Proxy Maybe -> Proxy Maybe In the expression: id In an equation for ‘foo’: foo = id Failed, modules loaded: none. }}} But this is peculiar, but it surely looks like `F` should be a type-level identity function! Of course, upon further inspection, we see that `F` is partial. It reduces only at kind `*`. This is quite hard to figure out, though, especially given that we're using the "default to `*`" behavior of open type families to arrange for this kind restriction. Thus, I propose: figure out when a type family reduction is held up due to a kind mismatch, and inform the user. -- Comment: This won't happen for 8.0.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ckoparkar): Hello. I'm a newcomer, and would like to give this a shot. As goldfire suggested, I've started looking at `TcErrors`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): A word of warning: TcErrors bears the accumulation of small patches that have been applied to incrementally improve error messages. I, personally, always find the module hard to navigate. However, if you have a specific erroneous situation in mind, it's not that hard to trace how that particular error filters through the module, and you should be able to find the stretch of code where the error itself is rendered. (A good starting place is to search for the text printed in the current error message.) To fix this, you'll have to add an extra check somewhere and then tailor the error message if necessary. Give a holler if you get stuck! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13192 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by v0d1ch): Hey @ckoparkar do you still work on this ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: v0d1ch Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by v0d1ch): * owner: (none) => v0d1ch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: v0d1ch Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Sasa asks (on ghc-devs) With the help of @int_index I found the place in TcErrors.hs where the error printing occurs and I think the check that I need to add will look similar to this one https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcErrors.hs#L1935. So I guess that we need to check if one of the kinds of two types we are comparing defaults to * (or Type if you will) and then add new warning that will be more descriptive as to why the failure happened. Maybe there is a way to check if what we are comparing are actually type families so that would make the job easier I guess. Richard replies I don't think the problem is particular to `Type` or defaulting. Instead, the problem is when * one of the two mismatched types is a type family application * and the type family has equations that pattern-match on an invisible parameter, * and it's that invisible-parameter matching that's gone awry. Now that I think about it, detecting these particular conditions might be tricky: you might need to edit code in `FamInstEnv` that does type family equation lookup to return diagnostic information if a match fails. (I would look at `reduceTyFamApp_maybe`, and perhaps it can return something more interesting than Nothing in the failure case.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: v0d1ch Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by v0d1ch): I have determined that in the failure case in this specific example we want the `Role` to be `Nominal` and we get a `[Type]` that looks like this: `[* -> *, Maybe]` while the `TyCon` is `F` How would I precede further with these informations ? I am also wondering if I should introduce new type that will give us the option to customize failure message instead of just `Nothing` ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10789: Notify user when a kind mismatch holds up a type family reduction -------------------------------------+------------------------------------- Reporter: goldfire | Owner: v0d1ch Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: newcomer, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13192 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire):
How would I proceed further with these informations ?
Not quite sure how to answer this. You might need to continue tracing the code path into `tcMatchTys`.
I am also wondering if I should introduce new type that will give us the
option to customize failure message instead of just `Nothing` ? Yes, I think so. For example, instead of `Nothing`, maybe it would work well to return an `Int` that gives the index of the first argument that mismatches. Then, the error-message generator could see if that index corresponds to an invisible argument; if so, suggest `-fprint-explicit- kinds`. Perhaps there's a better design, as well.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10789#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC