[GHC] #15515: Bogus "No instance" error when type families appear in kinds
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code typechecks: {{{#!hs {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy class C a where c :: Proxy a type family F data D :: F -> Type instance C (D :: F -> Type) where c = undefined }}} However, if we try to actually //use// that `C D` instance, like so: {{{#!hs c' :: Proxy (D :: F -> Type) c' = c @(D :: F -> Type) }}} Then GHC gives a rather flummoxing error message: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:20:6: error: • No instance for (C D) arising from a use of ‘c’ • In the expression: c @(D :: F -> Type) In an equation for ‘c'’: c' = c @(D :: F -> Type) | 20 | c' = c @(D :: F -> Type) | ^^^^^^^^^^^^^^^^^^^ }}} But that error is clearly misleading, as we defined such a `C D` instance directly above it! The use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | 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): The class instance should be rejected -- indeed, I'm quite surprised it's not. Let's write with explicit kinds: {{{#!hs class C k a where ... instance C (F -> Type) D where ... }}} That instance mentions a type family in one of its arguments, which should be rejected. I would love to come up with a way where we ignore determined dependent arguments during matching, which would then allow this instance to work, but we're not there yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | 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): Darn, I was afraid you were going to say that. Is there any relationship between this ticket and #12564? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | 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): Yes -- fixing that ticket will allow this one to make forward (as opposed to backward) progress. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: 12564 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * blockedby: => 12564 Comment: So as far as why GHC doesn't simply error when you define `instance C (D :: F -> Type)`, I think it might be due to these lines in `check_valid_inst_head`: {{{#!hs | otherwise = mapM_ checkValidTypePat ty_args where ... ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args }}} Where `checkValidTypePat` is what throws the `Illegal type synonym family application in instance` error seen in #12564. Because `ty_args` has filtered out kinds, it won't catch any type families in kinds, like in the original program. I think we could extend this error message to kinds by simply mapping `checkValidTypePat` over all `cls_args`, and not just `ty_args`. Do you agree? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: 12564 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, comment:4 seems right to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: 12564 | Blocking: Related Tickets: | Differential Rev(s): Phab:D5068 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5068 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15515: Bogus "No instance" error when type families appear in kinds
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler (Type | Version: 8.4.3
checker) | Keywords: TypeInType,
Resolution: | TypeFamilies
Operating System: Unknown/Multiple | Architecture:
Type of failure: Poor/confusing | Unknown/Multiple
error message | Test Case:
Blocked By: 12564 | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5068
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
#15515: Bogus "No instance" error when type families appear in kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeInType, Resolution: fixed | 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): Phab:D5068 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => closed * resolution: => fixed * blockedby: 12564 => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15515#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC