[GHC] #12384: Type family not reduced, again
#12384: Type family not reduced, again -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Linux Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This one looks similar to #12381, but unfortunately, it does not seem to be fixed in HEAD: {{{#!hs {-# LANGUAGE TypeInType, TypeFamilies, FlexibleInstances #-} import GHC.Types type family F (a :: Type) :: Type class C a where type D (a :: Type) :: F a instance (F a ~ Bool) => C a where type D a = True }}} This yields (in 8.0.1 and 8.1.20160709): {{{ Constraint.hs:11:14: error: • Expected kind ‘F a’, but ‘'True’ has kind ‘Bool’ • In the type ‘True’ In the type instance declaration for ‘D’ In the instance declaration for ‘C a’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12384 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12384: Type family not reduced, again -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by kosmikus: @@ -14,1 +14,1 @@ - type D a = True + type D a = True New description: This one looks similar to #12381, but unfortunately, it does not seem to be fixed in HEAD: {{{#!hs {-# LANGUAGE TypeInType, TypeFamilies, FlexibleInstances #-} import GHC.Types type family F (a :: Type) :: Type class C a where type D (a :: Type) :: F a instance (F a ~ Bool) => C a where type D a = True }}} This yields (in 8.0.1 and 8.1.20160709): {{{ Constraint.hs:11:14: error: • Expected kind ‘F a’, but ‘'True’ has kind ‘Bool’ • In the type ‘True’ In the type instance declaration for ‘D’ In the instance declaration for ‘C a’ }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12384#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12384: Type family not reduced, again -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by alexvieth): #12381 and #11348 were all about the order in which instance declarations are checked, but this case seems to be something different. Here there's no choice but to check these declarations in the order that they're written: the type family, then the class, then the instance of that class. I suppose the type of `D ()` should be `(F a ~ Bool) => True` but as far as I know GHC can't handle such a thing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12384#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12384: Type family not reduced, again -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: Yes, I think this is something we simply don't support at all. Associated type declarations are just a way to remind you to add `type instance` decl for D whenever you make an `instance` decl for `C`. It's always equivalent to doing it separately, thus: {{{ type instance D a = True instance (F a ~ Bool) => C a where }}} And you can see that this isn't going to work. The point is that `(F a ~ Bool)` is has local evidence, bound by the dictionary lambda for the instance dfun. That evidence can't be used in a `type instance` decl. So I'll close this as invalid, but you can re-open as a feature request if (a) you think it's important, (b) you can specify what it does, and (c) you can extend System FC to support it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12384#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC