When `f` calls `helper`, there are lots and lots of `Int`s available:
#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): Replying to [comment:38 goldfire]: the one passed into `f` as well as all of the others. How is this problematic? `f` is free to pass any `Int` using `incoherentWith`. E.g.: {{{ f :: Int -> Int f x = incoherentWith (x * 2) helper helper :: Int => Int helper = reflect + 1 }}} Here `f = (+1) . (*2)`. It is the programmer's responsibility to make sure that no other `Int`s are available in any given context. This is my idea behind `incoherentWith`: it is an unsafe function that requires discipline from the programmer; same as `Given` from `reflection` today. The safe interface can be built on top.
Yes, `=>` should merely introduce an implicit argument, but GHC should not guess an implicit value when there is more than one option.
I propose no such thing. GHC shouldn't guess anything.
This brings us back to Simon's suggestion about singleton types. I conjecture that there is no way to identify all singleton types without user direction. We could have users write a `{-# SINGLETON Either () Void #-}` pragma. But then we haven't come very far, as I don't know a way to check whether a `SINGLETON` pragma is lying or telling the truth.
I suppose that what's important here is not how many values *inhabit* the type, but how many ways are there to construct an inhabitant. There are clearly numerous ways to write `instance Show T`, but there's only one instance available, therefore it can safely go to the left of `=>`.
I also want to amplify Issue 2 from comment:31 to make sure that `blah :: Ord a -> a -> Set a` gets a reasonable error message.
How about this: if a function is ill-typed, try replacing the first `->` with a `=>`. If this makes the function well-typed, adjust the error message accordingly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler