Opened 2 years ago

Last modified 2 years ago

#12823 new feature request

Inconsistency in acceptance of equality constraints in different forms

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

{-# 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

-- 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).

Change History (4)

comment:1 Changed 2 years ago 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.

comment:2 in reply to:  1 Changed 2 years ago by dfeuer

Replying to 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?

comment:3 Changed 2 years ago 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.)

{-# 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.

comment:4 Changed 2 years ago 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.

Note: See TracTickets for help on using tickets.