#11715: There's something fishy going on with Constraint -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: 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 bgamari): I just remembered another little nugget that I noticed during #11334: There is a bizarre order dependence to this bug. For instance, {{{#!hs main = do print $ typeof (proxy :: proxy (Eq int)) print $ typeof (proxy :: proxy Eq) }}} will emit, {{{ Proxy Constraint (Eq Int) Proxy (Constraint -> Constraint) Eq }}} Whereas if you flip the order of the `print`s (presumably such that the solver encounters `*` first rather than `Constraint`) you see what I reported in the ticket description, {{{ Proxy (* -> *) Eq Proxy * (Eq Int) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: There's something fishy going on with Constraint -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: 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 simonpj): Indeed; see this (in `Kind.hs`) {{{ Note [Kind Constraint and kind *] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The kind Constraint is the kind of classes and other type constraints. The special thing about types of kind Constraint is that * They are displayed with double arrow: f :: Ord a => a -> a * They are implicitly instantiated at call sites; so the type inference engine inserts an extra argument of type (Ord a) at every call site to f. However, once type inference is over, there is *no* distinction between Constraint and *. Indeed we can have coercions between the two. Consider class C a where op :: a -> a For this single-method class we may generate a newtype, which in turn generates an axiom witnessing C a ~ (a -> a) so on the left we have Constraint, and on the right we have *. See Trac #7451. Bottom line: although '*' and 'Constraint' are distinct TyCons, with distinct uniques, they are treated as equal at all times except during type inference. }}} This is a true wart, which I have always longed to expunge. And actually, now we heterogeneous equalities, maybe we can!! Perhaps we could have {{{ newtype C a :: Constraint = MkC (a->a) -- Not legal source code }}} leading to an axiom {{{ axC :: forall (a:*). (C a :: Constraint) ~R (a->a :: *) }}} That is, `*` and `Constraint` both classify values, but different kinds of values. Is that ok? Or, I suppose we could say {{{ type Constraint = TYPE ConstraintRep }}} That would be even better, because we can certainly have `Ord a -> a` (at least in Core), and even `((->) (Ord a))`. Does that seem plausible? I like it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: There's something fishy going on with Constraint -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: 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 simonpj): NB: as things stand, from `axC` we could deduce `Constraint ~N *`, which we definitely don't want. To solve this we could restrict the coercion language a little, so that you can't extract a kind equality from a representational type equality. (This might be good anyway. It's weird that you can currently get a ''nominal'' kind equality from a ''representational'' type equality. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: There's something fishy going on with Constraint -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: 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 simonpj): In a phone conversation yesterday we also developed an alternative plan to comment:5, namely '''make `Constraint` and `*` the same in Haskell'''. Thus: * `type Constraint = *`. So the two are the same even in source Haskell. * A type sig like `f :: Int => Int` becomes kind-correct. But we can still rejects it in `checkValidType`, in the same way that we reject higher-rank types when that extension is not enabled. Ditto `f :: Ord a -> Int` '''Disadvantages''' This signature for `f` is currently rejected as ill-kinded: {{{ type family F a :: Constraint type instance F Int = Ord Bool ... f :: F a -> a -- Currently ill-kinded }}} but would now be accepted, because `checkValidType` could not easily reject it. More seriously {{{ g :: F a => a -> a }}} would also be accepted even if `F` plainly returned types not constraints. '''Advantages''' * The proposal would eliminate the need for constraint tuples distinct from ordinary value tuples, which would be good. * If we were to silence `checkValidType` (with a language extension), it would also allow functions like {{{ reify :: c => c with :: c -> (c => r) -> r }}} which allow you to get a dictionary as a value, and use it elsewhere. Currently this requires the "Dict trick": {{{ data Dict c where Dict :: c => Dict c reifyD :: c => Dict c reifyD = Ditc withD :: Dict c -> (c => r) -> r withD Dict k = k }}} but the Dict trick actually does boxing and unboxing because it involves a `data` type. It would be more direct not to require this. * Another example: perhaps `TypeRep a` (the type) and `Typeable a` (the constraint) could be the same thing. Thus {{{ f :: TypeRep a => TypeRep b -> blah }}} would mean that the first arg was passed implicitly and the second implicitly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: 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 Iceland_jack): Replying to [comment:9 simonpj]:

* If we were to silence `checkValidType` (with a language extension), it would also allow functions like {{{ reify :: c => c with :: c -> (c => r) -> r }}}

This was one of my use cases for #11441, this would be an interesting solution and may supersede that part of the proposal. Would this be enabled for each module or as a pragma: {{{#!hs {-# ALLOWINVALIDTYPE f #-} f :: Int => Int f = undefined }}} Heck, it could go as far as *require* an ill-kinded type — `{-# INVALIDTYPE f #-}` — such that this would not compile: {{{#!hs {-# INVALIDTYPE f #-} f :: Int -> Int f = undefined }}} What would be the use of that? It's machine checkable and who knows what changed during refactoring, a reader won't have to guess if there is some funny business going on. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.0.1 => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: 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 Ben Gamari ): In [changeset:"aa611746aa860e1884c9ad623d6939791f2645ff/ghc" aa61174/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="aa611746aa860e1884c9ad623d6939791f2645ff" users-guide: Add references to various issues in bugs section Test Plan: Read it Reviewers: austin Reviewed By: austin Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D2052 GHC Trac Issues: #7411, #11197, #11554, #11715 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Would this change make reflection (the library) obsolete? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 see no need for writing a body neither for `reify` nor `with` -- just make them GHC primitives. As to what to do when multiple constraints are in scope, I think that GHC should refuse to compile: {{{ with (10 :: Int) $ with (20 :: Int) $ -- When GHC looks for an `Int` to satisfy -- the `Int =>` constraint, it finds both -- 10 and 20, so it's a compile-time error. (reify :: Int) }}} Am I missing something important? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): At definition site `F a` cannot satisfy the `a =>` constraint unless `F a ~ a` is also in scope (it's not), so there's no ambiguity here. The way I see it, when you instantiate `a` with `Int`, instance resolution is already done. Is this not the case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Yes, a `with` error is not a viable solution. Since we'd like to treat anything to the LHS of `=>` the same way, issuing an error would break this example: {{{ data SomeOrd a where SomeOrd :: Ord a => a -> SomeOrd a cmp :: SomeOrd a -> SomeOrd a -> Ordering cmp (SomeOrd a) (SomeOrd b) = -- Do we use an 'Ord a' dictionary from the first argument -- or the second argument? We know it's the same dictionary -- because class instances are coherent, but this might be -- not the case for values provided by `with`. compare a b }}} By the way, how does GHC currently decide which dictionary to use in the example above? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Points well taken, but I'm a little uncomfortable with the directional of travel, because we ''are'' making things worse: the `reflection` library depends critically on `unsafeCoerce`. If we implement `with`, then we've essentially blessed this operation as safe. So the behavior is the same, but what was previously considered unsafe is now safe. It doesn't sound great to me. The example in comment:23 is, in my view, an infelicity in the design of the language. I'm not convinced that rejecting `cmp` is a good idea, but it is dangerously implementation-dependent. Indeed in GHC the choice of `Ord` dictionary might change between minor releases or depending on what order functions are written in a module. Here's an idea, based on visible type application (that is, `id @Int :: Int -> Int`) that allows us to specify usually-inferred parameters: * Extend the visible type application mechanism to work with dictionaries (that is, constraints). * Add the ability to bind a variable to an inferred parameter in a pattern, with `@`. * Reject code that uses dictionaries ambiguously, now that we have a workaround. The example from comment:23 is now rejected. But here is the working version: {{{ cmp :: SomeOrd a -> SomeOrd a -> Ordering cmp (SomeOrd @_ @d1 a) (SomeOrd @_ @_d2 b) = compare @_ @d1 a b }}} All the `@_` arguments above are because we don't care about the type variables, which come before the dictionaries. Here, we've explicitly chosen the first dictionary, so there is no ambiguity or implementation- dependence. Unfortunately, implementing this plan is a ways off. Perhaps we could just special-case `with` to error on ambiguity (naturally, this wouldn't break existing code) and know that we'll have a better solution later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Hm. Perhaps you're right that my suggestion goes against the spirit of Haskell constraints and that it would be more sensible to simply rename `with` to `incoherentWith`. Instead of my proposed error, we could simply add a warning when GHC detects (on a best effort basis) an ambiguous constraint. This warning would be triggered in `cmp`, for example, and silly uses of `incoherentWith`. Or perhaps not in `cmp` because GHC can detect that the ambiguously satisfied constraint is actually a class constraint and therefore assumed to be coherent. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): I have not read every word here, but to me it seems: * The main issue is whether `(Ord a)` is a singleton type. That is, if you have two `Ord` dictionaries around, does it matter which you choose? If it was a singleton, then `with` could not be incoherent. Of course, we can have two different `Ord` dictionaries by declaring two instances in different places. We could exclude that, if we wanted, by doing as we do with type families and checking for incompatible instances. But it's not a soundness issue so we don't. So, is that enough? Adding `with` does not make things any more incoherent, provided we limit the ways you can construct a value of kind `Constraint`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 ekmett): I have a couple of reservations about this ticket. Issue 1) {{{#!hs reify :: c => c with :: c -> (c => r) -> r }}} are morally close to `reflect` and `reify` from the `reflection` package respectively. (Chung-chieh Shan has a pretty compelling argument for why your `reify` is actually a `reflect`.) With the stated intent of working around the `Dict` hack, they work fine! However, they can also be used to model reflection in a dangerous way: By letting you pack up an arbitrary Int => ... now the instance for "Int" isn't unique. This means that the category of constraints isn't thin, and that now we care about provenance about where you got the Int from. This yields all the same problems as {{{#!hs class (?foo :: Int) => Bar a }}} from {{{#!hs class Int => Bar a }}} whereas we very explicitly disallow the former today. Right now every way you can compose an entailment in Constraint in the absence of IncoherentInstances and ImplicitParams is unique. This lets things like `Set` know the instance won't change on it between `insert` and `lookup`. I'm very scared of letting in something that would break that guarantee. Going the other way, and letting you bring constraints out to the right side of the => isn't hazardous, as with and reify don't give you tools to construct such a dictionary, and this just lets you move things around in the same manner as `Dict` does today. But with `Constraint = *`, it isn't clear how to keep that safe. `Given` in the `reflection` library, which provides this functionality today is actually being demoted to a supplemental package due to the amount of pain and confusion it causes users when multiple instances find themselves in scope. `reify` and `reflect` do not have those problems due to the quantifier. To preserve your desire to embed Constraint into * without overhead, in theory `Dict` could just be a magical newtype, put on and removed by the equivalent of your `reify` and `with` combinators: {{{ dict :: c => Dict c with :: Dict c -> (c => r) -> r }}} This avoids the `class Int => Bar a` issue entirely and doesn't interfere with a sound reflection story. Issue 2) It is a fairly common newbie error to write `foo :: Ord a -> a -> Set a` -- which would now very confusingly pass the type system rather than get caught. We should at least have the discussion about if this is desirable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Replying to [comment:32 simonpj]: This should work, although I would prefer to have `incoherentWith` at my disposal as well, for cases when I'm willing to manually ensure that in any local scope only one value is available. Consider this case: {{{ module M (f) where f :: Int -> ... helper1 :: Int => ... helper2 :: Int => ... }}} Here I'd like to pass `Int` to the helpers using `incoherentWith`, but since only `f` is exported, the unsafety is contained within the module boundaries. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Replying to [comment:34 rwbarton]:

I have a hard time believing you'd "like" to do this. Wouldn't it be more sensible to use implicit parameters?

I have a disdain for implicit parameters that stems from the fact that their names are represented by strings (`Symbol`s, to be precise), and names are not strings in my view, they are unique identifiers declared somewhere. More importantly, I may want to declare (unexported) data types in this module, and instances for those data types may require a context too: {{{ data Helper = ... instance Int => Eq Helper where ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 find pretending that `Int` is a constraint to be quite appealing, actually: it elevates the intuition that `=>` is like `->`, only implicit. The current design of `ImplicitParameters` will be easily expressible on top of this new feature with `(?param :: T) => t` desugaring into `Tagged "param" T =>` at type level and `?cmp` desugaring into `unTagged @"param" reflect` at term level. To sum it up, making `Type ~ Constraint` unifies/simplifies: * The `Dict` wrapper * `Typeable` & type-indexed `TypeRep` * `Given`-style and `Reifies`-style reflection * `-XImplicitParameters` To me, this kind of simplification is far from "distasteful". Meanwhile, I agree with issue (1) from comment:31 and we should certainly document to what problems `incoherentWith` leads, and actively discourage its incorrect use. I wouldn't be happy if people started using it to model implicits from Scala (which are basically incoherent type classes). It's still a useful function to have, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

When `f` calls `helper`, there are lots and lots of `Int`s available:

#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): Replying to [comment:38 goldfire]: the one passed into `f` as well as all of the others. How is this problematic? `f` is free to pass any `Int` using `incoherentWith`. E.g.: {{{ f :: Int -> Int f x = incoherentWith (x * 2) helper helper :: Int => Int helper = reflect + 1 }}} Here `f = (+1) . (*2)`. It is the programmer's responsibility to make sure that no other `Int`s are available in any given context. This is my idea behind `incoherentWith`: it is an unsafe function that requires discipline from the programmer; same as `Given` from `reflection` today. The safe interface can be built on top.

Yes, `=>` should merely introduce an implicit argument, but GHC should not guess an implicit value when there is more than one option.

I propose no such thing. GHC shouldn't guess anything.

This brings us back to Simon's suggestion about singleton types. I conjecture that there is no way to identify all singleton types without user direction. We could have users write a `{-# SINGLETON Either () Void #-}` pragma. But then we haven't come very far, as I don't know a way to check whether a `SINGLETON` pragma is lying or telling the truth.

I suppose that what's important here is not how many values *inhabit* the type, but how many ways are there to construct an inhabitant. There are clearly numerous ways to write `instance Show T`, but there's only one instance available, therefore it can safely go to the left of `=>`.

I also want to amplify Issue 2 from comment:31 to make sure that `blah :: Ord a -> a -> Set a` gets a reasonable error message.

How about this: if a function is ill-typed, try replacing the first `->` with a `=>`. If this makes the function well-typed, adjust the error message accordingly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

if a function is ill-typed, try replacing the first -> with a =>. If

#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 goldfire): Ah. I suppose comment:40 was clear from the beginning, but your {{{ f :: Int -> ... helper :: Int => ... }}} (without bodies) confused me. Perhaps we can phrase your intent in terms of implicit parameters: a "type" (as opposed to a constraint) appearing left of `=>` is just like an implicit parameter with a distinguished name `""`. Now, understanding `with 3 $ with 4 $ ...` is easy: the `...` will have access to `4`, which shadows `3`. I'm not saying it would necessarily be ''implemented'' like implicit parameters, but our understanding of IPs can inform this new feature. As for your suggestion this makes the function well-typed, adjust the error message accordingly. I'm afraid this would be hard to implement, because types can appear in so many different contexts. But here's an idea: We add a "validity" check -- something not really part of the type system -- that looks for types like `Ord a -> a -> Set a`. The validity check will fail if it sees a type to the left of an `->` that is headed by a class. To disable the validity check, enable `-XExplicitDictionaries`. But the error message would suggest using `=>` more prominently than enabling `-XExplicitDictionaries`! This validity check might not catch all cases all the time, but it would catch the common newbie error Edward brought up. Thinking about `Int =>` as a special implicit parameter makes this more palatable to me, somehow. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Perhaps the user guide is deficient with regard to implicit parameter shadowing. Maybe it's not even reliable -- I'm not sure. As for your first paragraph, I'm not convinced yet: `Int` is not like any other constraint, in that it's not a class. In GHC 8.0, we have a few forms of constraint: 1. Fully-applied classes 2. Implicit parameters 3. Tuples (which is actually special syntax for (1)) 4. Equality constraints 5. Other built-in constraints (`Coercible`, `Typeable`, are there more?) 6. Type families and synonyms which produce constraints You are advocating for something new: 7. Other Haskell types We thus can choose how to handle case (7) independently of how we handle other constraints, just like (2) has different "shadowing" behavior than (1). So `Int` will always be different from `Given Int`, and I think that's OK. As long as implicit parameters are around, then we've already lost the thinness of constraints. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:43 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Changes (by sweirich): * cc: sweirich (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:45 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Simon and I recently hit on a possible solution to this long-standing infelicity. 1. Add a new constructor of `RuntimeRep` (of levity-polymorphism fame), `ConstraintRep`. We would then have `type Constraint = TYPE ConstraintRep`. Even though values of types of kind `Constraint` have the same runtime representation as values of types of kind `Type`, it is still OK to have ''more'' distinctions in the type system than are needed at runtime. With this change, we can have things like `Num a -> a` in Core (where there is no distinction between `=>` and `->`), and this would be well- kinded because `->` simply requires that both types have a kind of the form `TYPE blah` for some `blah`. GHC currently desugars one-method (and 0-superclass) classes to be newtypes, not proper datatypes. This is more efficient, of course, than making a new box to store the dictionary. But it means under this new scheme that we have a heterogeneous newtype coercion. For example: {{{#!hs class C a where meth :: a -> a }}} is desugared into {{{#!hs newtype C a = MkCDict { meth :: a -> a } }}} which produces a coercion {{{ axC :: forall (a :: Type). C a ~R# (a -> a) }}} Under our new scheme, this coercion would be heterogeneous, because `C a :: TYPE ConstraintRep` and `(a -> a) :: TYPE LiftedRep`. Of course, GHC (now) handles heterogeneous equalities just fine, but there is a problem: GHC can extract a kind equality from a type equality via its `KindCo` coercion, captured in this typing rule: {{{ co : (t1 :: k1) ~r# (t2 :: k2) ----------------------------------------- KindCo co : (k1 :: Type) ~N# (k2 :: Type) }}} Note that the premise does not require any particular role on the coercion, while the conclusion is always nominal. With `KindCo` (and a few other coercion formers), we could derive a proof of `ConstraintRep ~N# LiftedRep` from `axC`. This is terrible. So: 2. Require the coercion in `KindCo` to be nominal. This makes our equality relation a tiny bit weaker, but I don't think the lost expressiveness will ever bite. GHC does not currently export a heterogeneous version of representational equality (although such a thing exists internally), so users can't every really witness it. And the place where this is key is in decomposing `AppCo`s, but the roles around `AppCo`s mean that the coercion relating the arguments is always nominal. So I think it will work out; building GHC's libraries with this restriction should be an adequate test. One remaining problem is that GHC uses newtype axioms for substitutions in, e.g., newtype unwrapping/normalization. So a heterogeneous axiom is a bad idea. And I'm not yet sure how to fix this. The normal way to avoid heterogeneity is just to cast one side. But we can't do this here, because the coercion we would have to use proves that `Constraint ~N# Type`, which is precisely what we are trying to avoid! So I'm still a bit stuck on this point. Another possible way forward is to do (1), above, and stop encoding one- element classes as newtypes. This has negative performance implications, and so that makes me sad. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:47 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Let's imagine a future where `(->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep). TYPE r1 -> TYPE r2 -> Type`. Then, we have the well-typed `(->) ConstraintRep LiftedRep (C a) (a -> a)`. But if we normalize w.r.t. newtypes (e.g., in `normaliseFfiType`), then we'll get `(->) ConstraintRep LiftedRep (a -> a) (a -> a)`, which is ill-kinded. In this case, we can just change `ConstraintRep` to `LiftedRep` as we normalize, but it's not clear that it will always be so easy. (But maybe it really will be, because we tend not to unwrap newtypes under other type constructors.) There's also the niggling problem that the type safety proofs in the presence of newtype axioms explicitly assume that axioms are homogeneous. But maybe this is unnecessary. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:49 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Flipping back through this ticket, I see that my new comment:47 seems to appear out of the blue. I also see @int-index advocating for dropping the distinction between `Constraint` and `Type` entirely.... but a quick skim doesn't show others agreeing with this direction of travel. I ''do'' think @int-index's approach (allowing `Int => ...`) is plausible, but I still am not convinced it's a good idea. If it's the ''only'' way to solve the original ticket, then perhaps it would be worth revisiting, but I'm not keen to start down that road. @int-index, you have argued well for your cause, but I, personally, need to see others agree with you and want these features before getting on board. It's not a matter of soundness or implementation, but of the kind of features and properties we wish Haskell to have. Responding more directly to comment:50: 1. That's true I suppose. We could also say, though, that `RuntimeRep` tells us the calling convention, not just the runtime representation. Constraints and regular types ''do'' have different calling conventions in Haskell code. 2. This goes back to my paragraphs above, in this comment. 3. `reflection` is an abuse of GHC, using an undocumented feature of the implementation. I do understand that many people use this undocumented feature, and so we could look at a way of saving `reflection`, but I don't see this as an argument against my proposal. We could always come up with another way to support `reflection` without newtype-classes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:51 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): Yes, it would work to have `TYPE :: Coherency -> RuntimeRep -> Type` instead of the current `TYPE :: RuntimeRep -> Type`. Algebraically, this is just the same as adding more constructors to `RuntimeRep`, as Simon and I have proposed. But I see how this might be preferable. I'm curious for Simon's opinion on this, noting that such a design is independent of the ability to use `Constraint`s to the left of `->` or `Type`s to the left of `=>`. This new design does not solve the problem I outline at the end of comment:47 though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:53 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Nevermind, it seems that this leads to the problem described in comment:6. Type families with domain `Type` can distinguish between between `Constraint` and `Type` in surface Haskell, so this difference needs to remain in Core. And in comment:7 I see Simon advocating the same change to KindCo as you describe. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:55 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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) | Keywords: Typeable, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: Typeable => Typeable, LevityPolymorphism -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:57 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism 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 bgamari): While speaking to danharaj about #10359 it occurred to me that the semantic issues with the tuple transform that simonpj proposes in ticket:10359#comment:2 would disappear if dictionaries were instead of kind `UnliftedPtrRep`. We could then introduce a core-to-core pass which would look for reconstructions of unlifted data constructors (e.g. `(case d of (a,b) -> a, case d of (a,b) -> b)`) and reduce them safely (e.g. to `d`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:59 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism 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 goldfire): I have made a [https://github.com/ghc-proposals/ghc-proposals/pull/32 ghc- proposal] about this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:61 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.1 => 8.4.1 Comment: This was a bit trickier than we anticipated and consequently we will be punting it to 8.4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:63 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism 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 simonpj): Using homogeneous coercions means that `KindCo` is gone; and that in turn perhaps means that the difficulties with using ''representational'' casts in types might go away. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:65 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles 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 simonpj): Just to record that Richard and I agreed that `constrainKind` currently has a bug. If `co :: Constraint ~ TYPE r`, then {{{ coercionKind (mkNthCo 0 (mkKindCo co)) }}} should succeed with `LiftedRep ~ r` but will fail because `Constraint` is syntactically `TYPE LiftedRep`. Stop-gap solution: * Make `coreView` do what `coreViewOneStarKind` does now; that is, expand `Constraint` to `TYPE LifteRep`. * Make the typechecker variants of `tcSplitTyConApp`, `tcSplitApp` use `tcView`; and make `tcView` '''not''' do this expansion. That is a more honest reflection of what is actually happening, until we fix it properly. Richard will have a go at this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:67 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles 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 goldfire): In cleaning up `tcView`/`coreView` to handle the disparity between the type-checker and Core vis-a-vis `Constraint`/`Type`, I came across a problem: which function (`coreView` or `tcView`) to use in the pure unifier? I decided that `coreView` was necessary there, because the pure unifier is used for instance overlap detection, where a `Constraint`/`Type` confusion could cause type unsoundness. But then `polykinds/T11480b` failed. A simplification of the problem is this: We have a class `C :: forall k. (Type -> k) -> Constraint`. The solver goes looking for an instance `C Constraint Eq`. (This instance is well-kinded.) But it finds an instance `C Type Eq`. As far as Core is concerned, this found instance is also well-typed... but the solver then looks at `C Type Eq` and falls over because the instance looks ill-kinded to it. One solution to this is to have the caller of any entry point into the pure unifier choose which notion of equality (i.e. `tcView`'s version or `coreView`'s version) it wants. But it's unclear what the right choices are. Here are the competing concerns: 1. We absolutely cannot have `type instance F Type = Int` and `type instance F Constraint = Bool`. That's begging for someone to write `unsafeCoerce`. 2. We also don't want the solver to find the instance for `C Type` when it goes looking for `C Constraint`, as that's very confusing to a solver that thinks `Type` and `Constraint` are different. 3. It would sure be nice to have both `Typeable Constraint` and `Typeable Type` be solvable. The only way I can think of resolving this is: - Forbid '''type''' instances that overlap w.r.t. `coreView`'s equality. - Allow '''class''' instances that overlap w.r.t. `coreView`'s equality. (After all, overlapping class instances can't cause unsoundness. - Use `tcView` when doing instance matching (for any instance flavor). This satisfies goals (1), (2), and (3). But it seems very squirrelly indeed to have different overlap checks for type instances and class instances. The only other alternative is to forbid `coreView` overlap for all instances and say that `Typeable Constraint` is insoluble, drastically reducing the set of `Typeable` things. I would love some thoughts from the crowd on this! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:69 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles 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 adamgundry): I'm inclined to agree with the proposal to use `coreView` in class/family instances, so we would regard an instance of `Typeable * Constraint` as overlapping `Typeable * Type` and hence not be able to solve the former. FWIW, here's an actual implementation of `unsafeCoerce` in GHC 8.0.2 exploiting this bug: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes, TypeFamilies, TypeOperators #-} import Data.Kind import Data.Typeable type family F x a b type instance F Type a b = a type instance F Constraint a b = b foo :: x :~: y -> F x a b -> F y a b foo Refl = id unsafeCoerce :: a -> b unsafeCoerce x = case eqT :: Maybe (Type :~: Constraint) of Nothing -> error "No more bug!" Just r -> foo r x }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:71 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles 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 goldfire): There is a counterargument to the need to find a ''sound'' solution. Assume `type family F`. In GHC 8.0, you can say {{{ type instance F Constraint = Int type instance F Type = Bool }}} In GHC 8.4, you will also be able to say this, as `Constraint` will be fully distinct from `Type`. But comment:69 and comment:70 propose to disallow these instances in 8.2. This is certainly quite strange from a user standpoint! Instead, perhaps we live with the unsoundness, as long as the user can't find out. My guess is that the user's only way of finding out is via `Typeable`, which would need to reinforced against such attacks. (Specifically, arrange to make sure that the rep for `Constraint` is distinct from that for `Type`.) But I think we can do this. I very much don't like the idea of unsoundness in Core, but it won't be the only way to implement `unsafeCoerce`, and continuing to allow those instances provides a smoother experience to the user. Credit to @yav, who provoked me into actually suggesting to live with unsoundness! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:73 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3316 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.4.1 => 8.6.1 Comment: Hopefully this will get done for 8.6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:77 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3316 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"c5d31df70b16dc346b5860077c8bbe585ddb7a78/ghc" c5d31df7/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="c5d31df70b16dc346b5860077c8bbe585ddb7a78" Treat isConstraintKind more consistently It turned out that we were not being consistent about our use of isConstraintKind. It's delicate, because the typechecker treats Constraint and Type as /distinct/, whereas they are the /same/ in the rest of the compiler (Trac #11715). And had it wrong, which led to Trac #15412. This patch does the following: * Rename isConstraintKind to tcIsConstraintKind returnsConstraintKind to tcReturnsConstraintKind to emphasise that they use the 'tcView' view of types. * Move these functions, and some related ones (tcIsLiftedTypeKind), from Kind.hs, to group together in Type.hs, alongside isPredTy. It feels very unsatisfactory that these 'tcX' functions live in Type, but it happens because isPredTy is called later in the compiler too. But it's a consequence of the 'Constraint vs Type' dilemma. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:81 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11621, #13742, | Differential Rev(s): Phab:D3316 #16139, #16148 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #11621, #13742 => #11621, #13742, #16139, #16148 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:83 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler