#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): I don't think that `cmp` should be rejected. I see no problem that GHC just picks one of the available dictionaries. Let me explain why. Currently, all of those types are equivalent: * `(a, b) => t` * `(b, a) => t` * `a => b => t` * `b => a => t` Also, those types are equivalent: * `c => t` * `(c, c) => t` * `c => c => t` This means that the only thing that identifies a value to the left of `=>` is its type. Whereas you can pass two distinct `Int`s to a function explicitly (`Int -> Int -> r`), you can't do the same implicitly (`Given Int => Given Int => r` ~ `Given Int => r`). It is therefore reasonable to expect that there's only *one unique value* of each type to the left of `=>`. If there are more, you can't distinguish between them anyway. This plays really well with type classes: since instances are coherent, `Ord a` is a unique value for each `a`. With the `Given`/`given`/`give` machinery from `reflection` we can now enrich the context with different values of the same type. I say that this is a violation of the philosophy behind `=>` and we don't want features (such as explicitly binding dictionaries using `@`-syntax) that get us further down this road. Partial solutions will not help. Say we forbid using nested `give`s with the same type as proposed in comment:22: the example in comment:24 demonstrates that we can violate the "one type - one value" principle without using nested `give`s by packaging the dictionaries in a GADT. I propose the following: let's get rid of `Given` and allow arbitrary things of kind `Type` to the left of `=>`. However, let's not call `give` some pretty name like `with` and add special casing; instead, let's call it `incoherentWithDict` and put it into a deep dark corner of `GHC.Exts`. Why bother at all? Now we can implement the safe interface (`Reifies`/`reflect`/`reify` from `reflection`) without `unsafeCoerce`, using `incoherentWithDict` instead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler