Constraint vs *

[bgamari]

I first noticed something was a bit odd with Constraint when chasing #11334. Consider this testcase (-O0 is sufficient),

import Data.Typeable

main = do
    print $ typeRep (Proxy :: Proxy Eq)
    print $ typeOf (Proxy :: Proxy Eq)

With ghc-8.0 this will produce,

Eq
Proxy (* -> *) Eq

Notice the second line; GHC seems to be claiming that Eq :: * -> *, which is clearly nonsense.

I believe this issue may be the cause of some of the testsuite failures that I'm seeing on #11011. Unfortunately I haven't the foggiest where this issue might originate.

See also

• #11621
• #12933
• #9547
• #13931
• #15918 (about mkCastTy)

[bgamari]

I just remembered another little nugget that I noticed during #11334: There is a bizarre order dependence to this bug. For instance,

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 prints (presumably such that the solver encounters * first rather than Constraint) all of the Constraintss magically turn into *,

Proxy (* -> *) Eq
Proxy * (Eq Int)

[bgamari]

So I believe that the culprit lies somewhere in the simplifier since the dump-ds output looks reasonable but dump-simpl reveals that the Typeable Proxy dictionary has been floated to the top level and has been applied to either * or Constraint, depending upon the order of the print statements, and that the same dictionary is used in both prints.

[goldfire]

I haven't looked at the code surrounding this, but here's a plausible story:

• * `eqType` Constraint evaluates to True, in case you didn't know. This fact is necessary in order to simplify Core more aggressively, as I understand it.

• The instance lookup mechanism looks for cached values. (See TcInteract, line 1306.) An instance for * will serve nicely as an instance for Constraint.

• So once an instance for * is found, that one is used for Constraint as well. This does not lead to any Core Lint problems (that is, it's perfectly type safe), because of my first bullet point.

Of course, * and Constraint are not equal in Haskell! One long-term solution I have for this is to make * ~R Constraint but not * ~N Constraint, as we have it now. But roles in kinds are most certainly a story for another day.

I do believe that a working solution is easy enough, though: just add a check, using tcEqType, in TcSMonad.findDict. tcEqType is careful not to relate * and Constraint. Recall that Core Lint can never check that we're doing this right, sadly.

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

[adamgundry]

The current behaviour definitely sounds suspicious. I notice that 8.0 RC2 accepts the following:

{-# LANGUAGE TypeInType, TypeFamilies #-}

import Data.Kind

type family F (a :: *) :: *
type instance F Type       = Int
type instance F Constraint = Bool

But surely if Type ~ Constraint in Core, and this definition is accepted, then Core is unsound? I'm not sure if this can be exploited in surface Haskell, but Ben's example makes me think it might.

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

[goldfire]

This was previously reported as #10075, but the commentary on that ticket adds little to the discussion here. I've closed the other ticket as a dup of this one.

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

[Iceland_jack]

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

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

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

[simonpj]

Combining Constraint with * would also

• resolve #9547

• Allow partial applications like (,) (Eq a) :: Constraint -> Constraint

[Ben Gamari <ben@…>]

In aa61174/ghc:

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

[int-index]

Would this change make reflection (the library) obsolete?

[goldfire]

How would we write the body for, say, with :: c -> (c => r) -> r? What about whichOne :: c -> c -> (c => r) -> r (which takes two elements of type c)?

I'm worried that the disadvantages of comment:11 are a bit painful. Perhaps no worse than where we are now, though.

[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?

[goldfire]

What about this:

type family F a where
  F Int = Int
  F a   = Char

foo :: F a -> a -> (a => r) -> r
foo x y k = with x $ with y $ k

When a is specialized to Int, the body of foo is ambiguous, even though it isn't under other conditions. How do we resolve this?

[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?

[goldfire]

Yes, that's true, but this is just the situation with IncoherentInstances, where specializing a type changes the meaning of an expression. Normally, we can assign an expression a more specific type at will. In this case, if we try to assign foo the more specific type Int -> Int -> (Int => r) -> r, we will get a duplicate-with error.

[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?

[int-index]

Here's a GHCi session you might find interesting. GHC just picks the first instance.

GHCi, version 8.1.20160813: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XGADTs
Prelude> :set -XFlexibleContexts 
Prelude> data X where X :: Given Int => X
Prelude> import Data.Reflection
Prelude Data.Reflection> data X where X :: Given Int => X
Prelude Data.Reflection> f X X = given :: Int
Prelude Data.Reflection> a = give (10 :: Int) X
Prelude Data.Reflection> b = give (20 :: Int) X
Prelude Data.Reflection> f a b
10
Prelude Data.Reflection> f b a
20

And here's the behavior of the type family example (when rewritten using reflection):

{-# LANGUAGE TypeFamilies, RankNTypes #-}

import Data.Reflection

type family F a where
  F Int = Int
  F a   = Char

foo :: F a -> a -> (Given a => r) -> r
foo x y k = give x $ give y $ k

GHCi, version 8.1.20160813: http://www.haskell.org/ghc/  :? for help
Prelude> :l With.hs 
[1 of 1] Compiling Main             ( With.hs, interpreted )
Ok, modules loaded: Main.
*Main> foo (10 :: Int) (20 :: Int) (given :: Int)
20

If you specialize foo by adding a ~ Int to its type signature, you get a different result!

foo :: (a ~ Int) => F a -> a -> (Given a => r) -> r
foo x y k = give x $ give y $ k

*Main> foo (10 :: Int) (20 :: Int) (given :: Int)
10

So, I say that the safe bet would be to *preserve* the current behavior, just get rid of Given. When multiple with are used, it is implementation defined which instance will get picked. Adding an equality constraint can indeed change the meaning of your code.

But this is already the case, so at least we're not making things worse.

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

[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 Ints 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 gives with the same type as proposed in comment:19: the example in comment:24 demonstrates that we can violate the "one type - one value" principle without using nested gives 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 create complex rules when it's allowed; instead, let's call it incoherentWith 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 incoherentWith instead.

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

[Iceland_jack]

Replying to int-index:

Currently, all of those types are equivalent:

• (a, b) => t
• (b, a) => t
• a => b => t
• b => a => t

Edwardk ​notes that a => b => t is slightly weaker than (a, b) => t since it can “only reference backwards up the chain” — I can't produce an example of this though. There may be differences between a => b => t and b => a => t as well.

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

[int-index]

Replying to goldfire:

A warning sounds like a plausible solution, provided that it's suppressed for class constraints.

---

Replying to Iceland_jack:

That's interesting, although I am not quite sure what "reference" means in this context.

---

Replying to simonpj:

Of course, we can have two different Ord dictionaries by declaring two instances in different places.

You can't have both of them in scope. And unless they are orphan instances, which are frowned upon, you can't use both of them in one program.

provided we limit the ways you can construct a value of kind Constraint.

If I understand correctly, the plan is to abolish kind Constraint in favor of Type. So with does make things more incoherent, as now you can have Int => t and Int is clearly not a singleton type, and you can have two distinct Ints in one scope.

[ekmett]

I have a couple of reservations about this ticket.

Issue 1)

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

class (?foo :: Int) => Bar a

from

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.

[simonpj]

Maybe we want with to work on only on singleton types, if we could somehow isolate those?

So rather than "be of kind Constraint" for with we need "is a singleton type"?

[int-index]

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

[rwbarton]

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

[int-index]

Replying to 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 (Symbols, 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
  ...

[rwbarton]

Well pretending Int is a constraint seems far more distasteful, and this whole discussion seems like a solution in search of a problem to me.

[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 => t at type level and ?param 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.

[goldfire]

While I certainly want to remove some of the ugliness around Constraint/Type, more clouds are appearing on the horizon. Specifically, I think

f :: Int -> ...
helper :: Int => ...

is problematic. When f calls helper, there are lots and lots of Ints available: the one passed into f as well as all of the others. Note that this is not the same with

g :: a -> (a => r) -> r

where only one value of type a is in scope. (Thanks, parametricity!)

Yes, => should merely introduce an implicit argument, but GHC should not guess an implicit value when there is more than one option. 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 also want to amplify Issue 2 from comment:31 to make sure that blah :: Ord a -> a -> Set a gets a reasonable error message.

[int-index]

Replying to goldfire:

When f calls helper, there are lots and lots of Ints available: 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 at most one Int is 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.

[int-index]

Oh, perhaps it's a miscommunication on my behalf. When I say "available in the context", by "context" I mean implicit parameters to the left of =>. So this should not compile:

f :: Int -> Int
f x =
  -- error: The 'Int =>' constraint is NOT satisfied by 'x'
  helper

helper :: Int => Int
helper = ...

[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

if a function is ill-typed, try replacing the first -> with a =>. If 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.

[int-index]

Replying to goldfire:

Now, understanding with 3 $ with 4 $ ... is easy: the ... will have access to 4, which shadows 3.

I am very suspicious about shadowing semantics. I'd rather see Int treated like any other constraint, no different than Given Int. We don't have shadowing semantics for Given Int: the example from comment:24 demonstrates that the first dictionary was picked, not the second one (and this behavior can change with a minor compiler version).

Once again, it moves us further down the road where we admit that there can be more than one value of one type to the left of =>. There shouldn't be. Well-defined semantics for using nested incoherentWith will encourage people to do so and thus violate this principle. In Edward's parlance, the Constraint category is thin; let's not change it.

I also couldn't find any mention of shadowing in the "Implicit parameters" section of the GHC user guide. Could you point me where I can read how it gets resolved? As far as I know, implicit parameters use the IP class under the hood, but GHC seems to consistently choose the innermost binding (in contrast to Given, where the outermost binding prevails):

GHCi, version 8.1.20160813: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XImplicitParams
Prelude> :set -XGADTs
Prelude> data X where X :: (?x :: Int) => X
Prelude> f :: X -> X -> Int; f X X = ?x
Prelude> f (let ?x = 1 in X) (let ?x = 2 in X)
2

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

[ekmett]

The main difference is that while we've lost the thinness of constraints in this narrow area, nobody uses them as they are largely regarded as a terrible idea with clunky syntax and, far more importantly, you explicitly can't actually use them as super-classes, so the damage is currently quite well contained.

[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:

class C a where
  meth :: a -> a

is desugared into

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 AppCos, but the roles around AppCos 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.

[simonpj]

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

Can you give an example?

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

[int-index]

I see a few problems with this approach:

1. RuntimeRep is used to distinguish things with different run-time representations. I understand why it's sound if things represented equally get different RuntimeReps, but it's not what RuntimeRep is for, so those fake inequalities are something to avoid (and you suggest to exploit it). Of course I understand that I'm in no position to tell you what RuntimeRep means because you invented it, but as a user I have certain expectations and intuition about what it means, and the name suggests that it means a run-time representation, not some arbitrary distinction which turned out to be convenient! A leaky abstraction.

2. I do think that having Constraint ~ * is useful in user code, because right now I have to use Dict to go from Constraint to * and Given to go in the opposite direction. It is very inconvenient!

3. We don't get the safe implementation of reflection (without unsafeCoerce) this way, do we? And if we stop encoding one-element classes as newtypes, the current implementation of reflection will break.

Making Constraint a synonym for * sounds very simple and elegant. What are the reasons to pursue a more complicated solution? It seems to me that all of the objections were addressed in this thread.

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

[int-index]

Couldn't we theoretically have constraints passed as unboxed data? In ​https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes I see that Edward Kmett suggests a separate flag to TYPE, Constraintiness, which would be more disciplined than misusing RuntimeRep and would solve the same problems.

Except I think that it should be called Coherency, not Constraintiness, because the main feature of things that go to the left of => is that they should have coherency properties (as was already discussed).

data Coherency = Coherent | Incoherent

This way we can even make -> coherency-polymorphic (and eliminate Dict, that would be safe). => could then require something Coherent, and -XIncoherentContexts (a companion to -XIncoherentInstances) could lift this restriction.

Then Int => would be disallowed unless the pragma is specified, but none of my objections would apply.

[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 Constraints to the left of -> or Types to the left of =>.

This new design does not solve the problem I outline at the end of comment:47 though.

[int-index]

Algebraically, this is just the same as adding more constructors to RuntimeRep

Well, yes, but

• you'd have to double the amount of constructors in RuntimeRep (coherent and incoherent version of each).

• more importantly, you couldn't be parametric in RuntimeRep and non-parametric in Coherency or vice versa.

This new design does not solve the problem I outline at the end of comment:47 though.

Forgive my ignorance, but is it necessary to have the same TYPE in Core as is in surface syntax? Couldn't we just "forget" the coherency annotation everywhere and translate surface TYPE :: Coherency -> RuntimeRep -> Type to TYPE :: RuntimeRep -> Type?

[int-index]

Nevermind, it seems that this leads to the problem described in comment:6. Type families with domain Type can distinguish between Constraint and Type in surface Haskell, so this difference must remain in Core.

And in comment:7 I see Simon advocating the same change to KindCo as you describe.

[goldfire]

Yes -- you've answered your own question correctly. And, yes, you're right about doubling the constructors, etc. I was just mentioning the algebraic correspondence mostly to convince myself that what you're proposing would clearly work (as well as what I've proposed), from a technical standpoint.

But it remains to be seen whether either approach really works out. I need to ponder this more and am curious for Simon's input.

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

[goldfire]

I have made a ​ghc-proposal about this.

[bgamari]

This was a bit trickier than we anticipated and consequently we will be punting it to 8.4.

[goldfire]

As comment:63 says, this patch (available on the wip/t11715 branch) is in limbo.

What's the challenge? See ​this comment on a related patch. The short version is that the design in comment:47 and in the ​ghc-proposal require weakening KindCo to work only on nominal coercions. And ​Phab:D2038 requires it to work on representational ones. The decision was to punt on this patch in favor of that one.

There is a somewhat-detailed plan of how to proceed, originally posted ​here:

1. Hold off on Constraint v Type until after the branch is cut.
2. Do what we can to mitigate Constraint v Type confusion vis-a-vis Typeable. (For example, make sure that there aren't Typeable instances for both, and have TcTypeable provide the Type instance whenever the Constraint instance is requested.)
3. Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous.
4. On the Constraint v Type patch, restore the full power of KindCo. This makes the type system broken, but I don't think the sky will come crashing down.
5. Merge Constraint v Type after the branch is cut. This will make GHC HEAD unsound in a new way, but no one will notice unless they try.
6. File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world).
7. Finish the first-class reification design and implement before 8.4.
8. Remove newtype-classes, thus eliminating heterogeneous axioms and the unsoundness mentioned in (5).

This plan was met with general applause.

But a recent chat with Simon suggested a new direction, that would allow us to separate Constraint from Type while keeping the efficiency of newtype-classes. In brief:

• Allow representational casts in kinds, resurrecting sections 5 and 6 of an ​unpublished paper of mine.

Currently, all kind-casts (that is, all uses of CastTy to change the kind of a type) use nominal coercions. This means that if we separate Constraint from Type, any equating of C a with a (in class C a where meth :: a) will somehow lead to a nominal equality between Constraint and Type, precisely the situation we wish to avoid. But if we allow representational coercions in kinds, then we can arrange to have Constraint ~R Type but not Constraint ~N Type. Indeed this makes more intuitive sense, because Constraint and Type do have the same runtime representation, but we wish to keep them separate regardless.

Sadly, representational coercions in kinds are troublesome, as described ​here and in that unpublished paper. The paper details a kind system that circumvents the problem, and thus presents a plausible way forward. But it requires yet more wrinkles in GHC's coercion language. Is this worth it? Perhaps. Previously, Simon vetoed that system as overly complicated. The nub of his argument was that there was no point in having roles in kind-coercions. But now, we have a reason to do this, so it might be well-advised to revisit that decision. It's also possible that any wisdom I have accumulated in the intervening years may come to bear and help us out.

Another approach that we considered was to have three different, unrelated arrow types: (->) :: TYPE r1 -> TYPE r2 -> Type, (=>) :: Constraint -> TYPE r -> Type, (=>) :: Constraint -> Constraint -> Type, where the last one is used to build dictionaries. Having these arrows like this prevents the need for KindCo to work on representational coercions -- thus removing the incompatibility between the original solution proposed in comment:47 and the work in ​Phab:D2038. This would work, and would allow us to keep C a ~R a, but then we couldn't have (C a => a) ~R (a -> a), so the newtype-class efficiency would run out of gas fairly quickly.

I do think, in the long run, that having representational coercions in kinds is the Right Answer, because it will be necessary to support promoting newtypes to kinds, necessary for full ​dependent types.

I don't expect any action on this until the summer, at least, but I wanted to jot it all down.

[simonpj]

Thoughts about the "representational casts in types" idea.

• We can't have just representational coercions in types, because to build some rep coercions we may need to give nominal coercions to a TyConAppCo. So we have to have both.

• 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. Or not

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

[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!

[simonpj]

Let me first note that we intend to make Constraint and Type distinct throughout the compiler. Then tcView = coreView again, and this entire problem goes away. We should not leave this too long.

Until then we are looking for a sound solution, but it doesn't have to be a good solution.

I'm puzzled about where the instance for C Type Eq comes from; after all, Eq :: Type -> Constraint.

I wonder what would go wrong if we just used coreView for both class and family instances. I think (3); but I still don't see an example except perhaps with a polykinded type constructor e.g. Typeable Type (Proxy Type) and Typeable Constraint (Proxy Constraint), and perhaps we can live with that for now.

[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:

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

[simonpj]

OK! Thanks for an exploitable test case!

[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!

[simonpj]

OK, so ​Phab:D3316 is a compromise fix for GHC 8.2. It re-introduces the tcView/coreView split, making Type and Constraint distinct in the typechecker and the same there after.

We regard this as a stop-gap solution, pending making Type and Constraint distinct througout the compiler.

However, T11480b currently fails with ​Phab:D3316: see comment:69 for why. The plan:

• Make the pure unifier use tcView not coreView. That should fix T11480b.

• Ensure that Typeable Type and Typeable Constraint produce different representations; that will fix comment:71 opf #11715

• Accept that a Core program can be unsound, in an obscure way, so long as the stop-gap solution holds. (We don't know any way to exploit this unsoundness from Haskell though.)

We should get on with the real solution for 8.4

[bgamari]

Hopefully this will get done for 8.6.

[bgamari]

Unmilestoning as no one is actively working on this.

[Simon Peyton Jones <simonpj@…>]

In c5d31df7/ghc:

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.