#9858: Typeable instances should be kind-aware -------------------------------------+------------------------------------- Reporter: dreixel | Owner: Type: bug | Status: merge Priority: highest | Milestone: 7.10.2 Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | typecheck/should_fail/T9858a, | should_run/T9858b | Blocking: | Differential Revisions: Phab:D652 -------------------------------------+------------------------------------- Comment (by oerjan): Let me elaborate on my previous comment, especially the first suggestion, since my hunch is that it requires the smallest changes to implement to get back constraint `Typeable`s: * Instead of prohibiting constraint `Typeable`s, ''detect'' the specific case of `Typeable (() :: Constraint)` and give it a different instance from `Typeable (() :: *)`. == Why is this not less secure than the current fix? == As shown in comment [comment:90], the current fix only effectively prohibits `Typeable` constraints for ''nullary'' constraint constructors. For other constraints, while ordinary users are greatly inconvenienced, an attacker can instead get the instances for all the constructors used (only the ''exact'' kind of `Constraint` is disallowed, not e.g. `* -> Constraint`) and put them together with type application, whose `Typeable` instance needs to be polymorphic and therefore cannot reasonably check for `Constraint` kinds. All nullary constructors ''other'' than `()` are either kind monomorphic or have kind parameters to distinguish the `TypeRep`s, so they are useless to an attacker. == How is it better? == It allows `Typeable` for constraints, which some people think are useful. My feeling is that constraints, especially used as type parameters, shouldn't be considered impredicative except ''possibly'' if they contain `=>`. Prohibiting this case was the 3rd suggestion, but my hunch is that this is a more complicated change, and might, if desired, be better done with an overall overhaul disallowing `=>` more uniformly in the same contexts as quantified types, including disallowing splitting `a => b` into a type application. == How does it still seem a bit awkward? == It still allows some types to have identical `TypeRep`s, like `(,) :: * -> * -> *` and `(,) :: Constraint -> Constraint -> Constraint`. This is no change from the current fix, though. Fixing this entirely was the 2nd suggestion. It might perhaps be implemented directly, although my hunch is that it requires more work, because it needs checking for partial applications and thus more complicated kinds. I assume Edward's suggestion automatically implies this. == How is it sufficient? == With either my suggestion or the currently implemented fix, although some types still have identical `TypeRep`s, I believe they can never have identical ''kinds'' as well, and all cast operations require the actual kinds of the compared `Typeable`s to be equal. '''Proposition''': If two types `t` and `u` have the property: * `t` and `u` are distinct as Haskell types, but have the same `TypeRep` under the pre-fix system, and ''either'' both have the same kind or one has kind `*` and the other has kind `Constraint`; then one of the following holds: * They have two corresponding type arguments with the same property. * They are, in some order, `() :: *` and `() :: Constraint`. '''Proof''': If at least one of `t` and `u` does ''not'' have as its tycon one of the kind-ambiguous types `(), (,), ..., (->), (=>)`, then to have equal `TypeRep`s, their tycons and lists of kindreps must be identical, and the types themselves and all their arguments must have corresponding kinds. Thus to be different as types two of their corresponding arguments must have the property. If the tycons ''are'' kind-ambiguous then any arguments must have kind either `*` or `Constraint`. With no arguments, with the ''exception'' of `()`, the types must have different kinds that are not `*` or `Constraint`, a contradiction. Otherwise, the kinds of the tycons are determined by the kinds of the first arguments, and for `t` and `u` to be distinct, there must be two corresponding arguments with the property. ---- To justify the possibility of the 3rd alternative suggestion as well, the above proof can be adjusted to show that if the kinds of `t` and `u` are ''equal'', then types of the form `a -> c` and `b => c` must appear as corresponding arguments at some step. This is because all the other options preserve whether the kinds of the arguments are equal or different. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9858#comment:92 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler