[GHC] #9858: Typeable instances should be kind-aware

[GHC]

#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