[GHC] #12823: Inconsistency in acceptance of equality constraints in different forms
#12823: Inconsistency in acceptance of equality constraints in different forms -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: GADTs | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently, we (correctly) require a language extension to accept a declaration like foo :: a ~ b => f a -> f b foo x = x Suppose I write {{{#!hs {-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-} module A where class a ~ b => Equal a b instance a ~ b => Equal a b type EqualS a b = a ~ b }}} and then {{{#!hs -- No extensions module B where -- This works useEqual :: Equal a b => f a -> f b useEqual x = x -- But this does not useEqualF :: EqualF a b => f a -> f b useEqualF x = x }}} It seems that GHC expands type synonyms, but does not reduce constraints, before deciding whether enough extensions are in play to allow equality constraints. This mismatch feels weird. Is there something about `~` proper, and not `Equal`, that triggers the difficulties with let generalization? If not, I think they should either both work or both fail (probably both fail). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12823 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12823: Inconsistency in acceptance of equality constraints in different forms -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I assume `EqualF` should be `EqualS`. As long as we're allowing the full application of a multiparameter type class in a module with no extensions in the first place (strictly speaking, it should be a syntax error in Haskell 2010), I see no purpose in rejecting either of your functions in module `B`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12823#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12823: Inconsistency in acceptance of equality constraints in different forms -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:1 rwbarton]:
I assume `EqualF` should be `EqualS`.
Indeed.
As long as we're allowing the full application of a multiparameter type class in a module with no extensions in the first place (strictly speaking, it should be a syntax error in Haskell 2010), I see no purpose in rejecting either of your functions in module `B`.
My concern: `GADTs` implies `MonoLocalBinds` because (for reasons I don't personally understand) GADTs don't play well with let generalization. Since the `Equal` class and `ExistentialQuantification` are sufficient to simulate GADTs, I would expect them to run into the same inference fragility issues without `MonoLocalBinds`. Am I missing something? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12823#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12823: Inconsistency in acceptance of equality constraints in different forms -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Hmm. GHC won't let you pattern match on a GADT in a module without `GADTs` or `TypeFamilies`. But you can emulate the GADT with `Equal` and an existential type as dfeuer says, and then GHC accepts the match and even does the type refinement without complaining. (But not if you use `EqualS`! Then GHC thinks the existential type is a GADT.) {{{#!hs {-# LANGUAGE GADTs #-} module G1 where class a ~ Int => IsInt a instance IsInt Int data X a = IsInt a => C --- module G2 where import G1 f :: X a -> a f C = 7 }}} This doesn't seem like a great situation, but you are allowed to turn off `MonoLocalBinds` explicitly in a module with `GADTs` already, so it's not so terrible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12823#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12823: Inconsistency in acceptance of equality constraints in different forms -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I agree it's a bit odd but I don't see how to do better. Generally, GHC's view is that the language-extension flags apply to the source code you write in the module being compiled; and NOT to the library code that you are implicitly using thereby. Type synonyms are very transparent, and hide nothing, which is a bit in conflict with the above. Perhaps we could make them opaque for the purpose of language-extension tests? I'm sure we'd get different complaints then :-). So I don't see a straightforward way to fix this inconsistency. Yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12823#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC