[GHC] #14968: QuantifiedConstraints: Can't be RHS of type family instances
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's a type family that I tried to write using QuantifiedConstraints. {{{#!hs {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE QuantifiedConstraints #-} module QCTypeInstance where import GHC.Exts (Constraint) type family Functors (fs :: [(* -> *) -> * -> *]) :: Constraint type instance Functors '[] = (() :: Constraint) type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) }}} Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition. {{{ $ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted ) QCTypeInstance.hs:13:15: error: • Illegal polymorphic type: forall (f :: * -> *). Functor f => Functor (t f) • In the type instance declaration for ‘Functors’ | 13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) | ^^^^^^^^ }}} Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #9269 Comment: This is a particular occurrence of a more general restriction, which is explained in https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1. So yes, there are fundamental difficulties here that have yet to be worked out. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by josef): Right. I'm aware to the difficulties discussed in ticket #9269. My questions is really whether we can hope to do better when the result kind of a type family is of kind `Constraint` rather than `*`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm not sure what the return kind has anything to do with this. Ultimately, the issue is impredicativity, which is going to be a problem regardless of whether you're working over `*`, `Constraint` (as in your example), `Bool` (as in the example in https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1), or something else. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Actually, I think the OP's use case should be OK. There is a big difference between the ''type'' `(forall x. x -> x, Int)` and the ''constraint'' `(forall x. A x => B x, Show x)`. The former is an impredicative use of the `(,)` constructor, while the second is not considered to be so. I think this is a simple case of updating the validity checker to allow the new thing. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm lost. Is there some aspect of quantified constraints that would make this OK: {{{#!hs type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) }}} But not this (from https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1)? {{{#!hs type instance Foo True = forall a. a -> a -> a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The challenge impredicativity causes is in knowing where there is an invisible parameter. (I'm pretty sure that's the challenge, at least.) So if `x :: ty` and we don't know whether or not `ty` is a `forall`-type, we have a problem. This simply doesn't happen with constraints, so we avoid the challenge. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 goldfire]:
This simply doesn't happen with constraints, so we avoid the challenge.
Really? Is there some sort of invariant in GHC that upholds this claim? You can certainly have `x :: ty` where `ty :: Constraint` in Core, so this claim is quite surprising to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): The challenge is knowing whether a type `(F t)` might reduce to a polytype. Currently that cannot happen. Allowing it to happen gives all the same problems as impredicativity in general. So I think that allowing a forall on the RHS of a `type instance` is a big step. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This compiles {{{#!hs type family Functors (fs :: [(Type -> Type) -> Type -> Type]) :: Constraint type instance Functors '[] = (() :: Constraint) type instance Functors (t:ts) = (LvlUp Functor t, Functors ts) class (forall x. cls x => cls (f x)) => LvlUp cls f instance (forall x. cls x => cls (f x)) => LvlUp cls f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * keywords: QuantifiedConstraints => QuantifiedConstraints wipT2893 Comment: Relevant discussion at ticket:14734#comment:5 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Well comment:9 doesn't have foralls on the RHS of a type family, so should be fine. I'm not sure how/why it's relevant to this thread though! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14968: QuantifiedConstraints: Can't be RHS of type family instances -------------------------------------+------------------------------------- Reporter: josef | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9269 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: QuantifiedConstraints wipT2893 => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14968#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC