subverting Data.Constraint.Forall to coerce between Int and Char

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
{-# LANGUAGE ConstraintKinds, TypeOperators, MultiParamTypeClasses,                                                                                                                                                
  OverlappingInstances, FlexibleInstances, TypeFamilies, Rank2Types, GADTs                                                                                                                                         
  #-}

-- I had to cheat, and use OverlappingInstances -- but Kmett left me no choice!

module SubvertInst where

import Data.Constraint
import Data.Constraint.Forall



-- below, we create this ~ dictionary. I'm pretty sure the definitions below                                                                                                                                       
-- could be massaged into a value of type (forall a b. Dict (a ~ b)), but                                                                                                                                          
-- @int_char@ is enough to demonstrate the attack vector.                                                                                                                                                          
int_char :: Dict (Char ~ Int)
int_char = trans_eq charEq intEq

-- here's a demonstration                                                                                                                                                                                          
main = putStrLn $ [coerce int_char 0]



-- some basic definitions we could have imported from other packages                                                                                                                                               
data PROXY a = PROXY

trans_eq :: Dict (a ~ x) -> Dict (b ~ x) -> Dict (a ~ b)
trans_eq Dict Dict = Dict

coerce :: Dict (a ~ b) -> b -> a
coerce Dict = id



-- this class with overlapping instances is our main attack vector                                                                                                                                                 
class IsEither a b x where
  cnv :: PROXY (a, b, x) -> Maybe (Dict (x ~ a))

instance IsEither a b a where cnv _ = Just Dict
instance IsEither a b b where cnv _ = Nothing



-- with the class, we can create these dictionaries...                                                                                                                                                             

--charEq :: Dict (Char ~ Data.Constraint.Forall.A)                                                                                                                                                                 
Just charEq = case x of
  Sub d -> case d of
    Dict -> cnv (prxChar x)

  where x = atChar (bad ())

--inEq :: Dict (Int ~ Data.Constraint.Forall.A)                                                                                                                                                                    
Just intEq = case x of
  Sub d -> case d of
    Dict -> cnv (prxInt x)

  where x = atInt (bad ())



-- we have to jump through hoops since Data.Constraint.Forall.{A,B} are not in                                                                                                                                     
-- scope; that's what all the rest of these definitions do                                                                                                                                                         
bad () = extract inst where
  extract :: (forall p x. (p sko1, p sko2) :- p x) ->
	(IsEither sko1 sko2 sko1, IsEither sko1 sko2 sko2) :- IsEither sko1 sko2 a
  extract inst = inst

atChar :: ((p sko1, p sko2) :- p Char) -> ((p sko1, p sko2) :- p Char)
atChar = id

atInt :: ((p sko1, p sko2) :- p Int) -> ((p sko1, p sko2) :- p Int)
atInt = id

prxChar :: ((p sko1, p sko2) :- p a) -> PROXY (sko1, sko2, Char)
prxChar _ = PROXY

prxInt :: ((p sko1, p sko2) :- p a) -> PROXY (sko1, sko2, Int)
prxInt _ = PROXY