Opened 3 years ago
Last modified 6 weeks ago
#11715 new bug
Constraint vs *
Reported by: | bgamari | Owned by: | goldfire |
---|---|---|---|
Priority: | high | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.1-rc1 |
Keywords: | Typeable, LevityPolymorphism, Roles | Cc: | adamgundry, sweirich, RyanGlScott, jmgrosen |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #11621, #13742, #16139, #16148 | Differential Rev(s): | Phab:D3316 |
Wiki Page: |
Description (last modified by )
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
Change History (83)
comment:2 Changed 3 years ago by
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 print
s.
comment:3 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:4 Changed 3 years ago by
I haven't looked at the code surrounding this, but here's a plausible story:
* `eqType` Constraint
evaluates toTrue
, 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 forConstraint
.
- So once an instance for
*
is found, that one is used forConstraint
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.
comment:5 Changed 3 years ago by
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.
comment:6 Changed 3 years ago by
Cc: | adamgundry added |
---|
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.
comment:7 Changed 3 years ago by
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.
comment:8 Changed 3 years ago by
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.
comment:9 follow-up: 11 Changed 3 years ago by
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 incheckValidType
, 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 likereify :: 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 adata
type. It would be more direct not to require this.
- Another example: perhaps
TypeRep a
(the type) andTypeable a
(the constraint) could be the same thing. Thusf :: TypeRep a => TypeRep b -> blah
would mean that the first arg was passed implicitly and the second implicitly.
comment:10 Changed 3 years ago by
Summary: | There's something fishy going on with Constraint → Constraint vs * |
---|
comment:11 Changed 3 years ago by
Replying to simonpj:
- If we were to silence
checkValidType
(with a language extension), it would also allow functions likereify :: 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.
comment:12 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:13 Changed 3 years ago by
Milestone: | 8.0.1 → 8.2.1 |
---|
comment:14 Changed 3 years ago by
Combining Constraint
with *
would also
- resolve #9547
- Allow partial applications like
(,) (Eq a) :: Constraint -> Constraint
comment:16 Changed 3 years ago by
Keywords: | Typeable added |
---|
comment:18 Changed 3 years ago by
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.
comment:19 Changed 3 years ago by
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?
comment:20 Changed 3 years ago by
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?
comment:21 Changed 3 years ago by
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?
comment:22 Changed 3 years ago by
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.
comment:23 Changed 2 years ago by
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?
comment:24 Changed 2 years ago by
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.
comment:25 Changed 2 years ago by
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.
comment:26 follow-up: 28 Changed 2 years ago by
I don't think that cmp
should be rejected. I see no problem that GHC just picks one of the available dictionaries. Let me explain why.
Currently, all of those types are equivalent:
(a, b) => t
(b, a) => t
a => b => t
b => a => t
Also, those types are equivalent:
c => t
(c, c) => t
c => c => t
This means that the only thing that identifies a value to the left of =>
is its type. Whereas you can pass two distinct Int
s to a function explicitly (Int -> Int -> r
), you can't do the same implicitly (Given Int => Given Int => r
~ Given Int => r
). It is therefore reasonable to expect that there's only *one unique value* of each type to the left of =>
. If there are more, you can't distinguish between them anyway. This plays really well with type classes: since instances are coherent, Ord a
is a unique value for each a
.
With the Given
/given
/give
machinery from reflection
we can now enrich the context with different values of the same type. I say that this is a violation of the philosophy behind =>
and we don't want features (such as explicitly binding dictionaries using @
-syntax) that get us further down this road.
Partial solutions will not help. Say we forbid using nested give
s with the same type as proposed in comment:19: the example in comment:24 demonstrates that we can violate the "one type - one value" principle without using nested give
s by packaging the dictionaries in a GADT.
I propose the following: let's get rid of Given
and allow arbitrary things of kind Type
to the left of =>
. However, let's not call give
some pretty name like with
and 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.
comment:27 Changed 2 years ago by
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.
comment:28 Changed 2 years ago by
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.
comment:29 follow-up: 30 Changed 2 years ago by
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 twoOrd
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
.
comment:30 Changed 2 years ago by
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 Int
s in one scope.
comment:31 Changed 2 years ago by
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.
comment:32 follow-up: 33 Changed 2 years ago by
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"?
comment:33 Changed 2 years ago by
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.
comment:34 follow-up: 35 Changed 2 years ago by
I have a hard time believing you'd "like" to do this. Wouldn't it be more sensible to use implicit parameters?
comment:35 Changed 2 years ago by
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 (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 ...
comment:36 Changed 2 years ago by
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.
comment:37 Changed 2 years ago by
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-indexedTypeRep
Given
-style andReifies
-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.
comment:38 follow-up: 39 Changed 2 years ago by
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 Int
s 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.
comment:39 Changed 2 years ago by
Replying to goldfire:
When
f
callshelper
, there are lots and lots ofInt
s available: the one passed intof
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 aSINGLETON
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.
comment:40 Changed 2 years ago by
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 = ...
comment:41 follow-up: 42 Changed 2 years ago by
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.
comment:42 Changed 2 years ago by
Replying to goldfire:
Now, understanding
with 3 $ with 4 $ ...
is easy: the...
will have access to4
, which shadows3
.
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
comment:43 Changed 2 years ago by
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:
- Fully-applied classes
- Implicit parameters
- Tuples (which is actually special syntax for (1))
- Equality constraints
- Other built-in constraints (
Coercible
,Typeable
, are there more?) - Type families and synonyms which produce constraints
You are advocating for something new:
- 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.
comment:44 Changed 2 years ago by
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.
comment:45 Changed 2 years ago by
Cc: | sweirich added |
---|
comment:46 Changed 2 years ago by
Cc: | RyanGlScott added |
---|
comment:47 Changed 2 years ago by
Simon and I recently hit on a possible solution to this long-standing infelicity.
- Add a new constructor of
RuntimeRep
(of levity-polymorphism fame),ConstraintRep
. We would then havetype 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:
- 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.
comment:48 Changed 2 years ago by
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?
comment:49 Changed 2 years ago by
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.
comment:50 Changed 2 years ago by
I see a few problems with this approach:
RuntimeRep
is used to distinguish things with different run-time representations. I understand why it's sound if things represented equally get differentRuntimeRep
s, but it's not whatRuntimeRep
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 whatRuntimeRep
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.
- I do think that having
Constraint ~ *
is useful in user code, because right now I have to useDict
to go fromConstraint
to*
andGiven
to go in the opposite direction. It is very inconvenient!
- We don't get the safe implementation of
reflection
(withoutunsafeCoerce
) this way, do we? And if we stop encoding one-element classes as newtypes, the current implementation ofreflection
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.
comment:51 Changed 2 years ago by
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:
- 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.
- This goes back to my paragraphs above, in this comment.
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 savingreflection
, but I don't see this as an argument against my proposal. We could always come up with another way to supportreflection
without newtype-classes.
comment:52 Changed 2 years ago by
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.
comment:53 Changed 2 years ago by
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.
comment:54 Changed 2 years ago by
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 inCoherency
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
?
comment:55 Changed 2 years ago by
comment:56 Changed 2 years ago by
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.
comment:57 Changed 2 years ago by
Keywords: | LevityPolymorphism added |
---|
comment:58 Changed 2 years ago by
Owner: | set to goldfire |
---|
comment:59 Changed 2 years ago by
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
).
comment:60 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:62 Changed 2 years ago by
Priority: | high → highest |
---|
comment:63 Changed 2 years ago by
Milestone: | 8.2.1 → 8.4.1 |
---|
This was a bit trickier than we anticipated and consequently we will be punting it to 8.4.
comment:64 Changed 2 years ago by
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:
- Hold off on Constraint v Type until after the branch is cut.
- 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.)
- Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous.
- 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.
- 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.
- File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world).
- Finish the first-class reification design and implement before 8.4.
- 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.
comment:65 Changed 2 years ago by
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
comment:66 Changed 2 years ago by
Keywords: | Roles added |
---|
comment:67 Changed 2 years ago by
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 whatcoreViewOneStarKind
does now; that is, expandConstraint
toTYPE LifteRep
.
- Make the typechecker variants of
tcSplitTyConApp
,tcSplitApp
usetcView
; and maketcView
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.
comment:68 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:69 Changed 2 years ago by
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:
- We absolutely cannot have
type instance F Type = Int
andtype instance F Constraint = Bool
. That's begging for someone to writeunsafeCoerce
.
- We also don't want the solver to find the instance for
C Type
when it goes looking forC Constraint
, as that's very confusing to a solver that thinksType
andConstraint
are different.
- It would sure be nice to have both
Typeable Constraint
andTypeable 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!
comment:70 Changed 2 years ago by
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.
comment:71 Changed 2 years ago by
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
comment:73 Changed 2 years ago by
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!
comment:74 Changed 23 months ago by
Differential Rev(s): | → Phab:D3316 |
---|
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
notcoreView
. That should fixT11480b
.
- Ensure that
Typeable Type
andTypeable 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
comment:75 Changed 20 months ago by
Description: | modified (diff) |
---|
comment:76 Changed 19 months ago by
Cc: | jmgrosen added |
---|
comment:78 Changed 11 months ago by
Milestone: | 8.6.1 |
---|---|
Priority: | highest → high |
Unmilestoning as no one is actively working on this.
comment:79 Changed 9 months ago by
Blocking: | 15198 added |
---|
comment:80 Changed 9 months ago by
Blocking: | 15198 removed |
---|
comment:82 Changed 3 months ago by
Related Tickets: | → #11621, #13742 |
---|
comment:83 Changed 6 weeks ago by
Related Tickets: | #11621, #13742 → #11621, #13742, #16139, #16148 |
---|
I just remembered another little nugget that I noticed during #11334: There is a bizarre order dependence to this bug. For instance,
will emit,
Whereas if you flip the order of the
print
s (presumably such that the solver encounters*
first rather thanConstraint
) all of theConstraints
s magically turn into*
,