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