@@ -0,0 +1,115 @@
1+-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving #-}
3+
4+module TySet(plugin, Set, Union) where
5+
6+import TypeRep
7+import Type
8+import Kind
9+import TcEvidence
10+import CoAxiom
11+import Name
12+import OccName
13+import Var
14+import TyCon
15+import BasicTypes
16+
17+-- friends:
18+import Var
19+import VarEnv
20+import VarSet
21+import Name
22+import BasicTypes
23+import TyCon
24+import Class
25+import CoAxiom
26+
27+-- others
28+import PrelNames
29+import Outputable
30+import FastString
31+import Util
32+import DynFlags
33+
34+import TcPluginM ( TcPluginM, tcPluginIO, tcPluginTrace )
35+import TcRnMonad ( TcPlugin(..), TcPluginResult(..)
36+ , Ct(..), CtEvidence(..), CtLoc, ctLoc, ctPred
37+ , mkNonCanonical, isTouchableTcM, unsafeTcPluginTcM)
38+import Plugins ( CommandLineOption, defaultPlugin, Plugin(..) )
39+
40+import Debug.Trace
41+import Outputable
42+import DynFlags
43+
44+import Control.Monad
45+import qualified Data.Typeable as DT
46+
47+{- Set constructor -}
48+data Set (a :: [k])
49+{- Union operation -}
50+type family Union (a :: [k]) (b :: [k]) :: [k]
51+
52+{- Plugin setup -}
53+plugin :: Plugin
54+plugin = defaultPlugin { tcPlugin = Just . thePlugin }
55+
56+thePlugin :: [CommandLineOption] -> TcPlugin
57+thePlugin opts = TcPlugin
58+ { tcPluginInit = pluginInit opts
59+ , tcPluginSolve = pluginSolve
60+ , tcPluginStop = pluginStop
61+ }
62+
63+pluginInit :: [CommandLineOption] -> TcPluginM ()
64+pluginInit _ = return ()
65+
66+pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
67+pluginSolve () given derived wanted =
68+ do -- For debugging, show the constraints
69+ tcPluginTrace "SET" $ ppCts wanted
70+ tcPluginTrace "SET" $ ppr $ head $ wanted
71+ solved <- findSetEquality wanted
72+ -- For the sake of debugging
73+ tcPluginIO $ putStrLn "Running Set equality plugin"
74+ return $ TcPluginOk solved []
75+
76+-- Pretty print constraints
77+ppCts [] = text "(empty)"
78+ppCts cs = vcat (map ppr cs)
79+
80+{- Some debugging Show instances to help me understand what is coming in and out of GHC -}
81+deriving instance Show TyLit
82+deriving instance Show Type
83+instance Show Var where
84+ show v = showSDocUnsafe $ ppr v
85+instance Show TyCon where
86+ show tycon = showSDocUnsafe $ ppr tycon
87+
88+-- Prediacate one whether a type is = Set '[]
89+isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
90+ guard $ length tcs == 2
91+ guard $ getOccString (tyConName x) == "Set"
92+ case tcs of [TyVarTy k, TyConApp con [TyVarTy k']] ->
93+ do guard $ k == k'
94+ guard $ (getOccString . tyConName $ con) == "[]"
95+ _ -> Nothing
96+
97+{- Experimenting, finds Set '[] ~ Set '[] and returns a refl coercion
98+ This was set up before when 'Set' was a type family, but is now redundant
99+-}
100+findSetEquality :: [Ct] -> TcPluginM [(EvTerm, Ct)]
101+findSetEquality [] = return []
102+findSetEquality (ct : xs) = let x = (do (Nominal,t1,t2) <- getEqPredTys_maybe (ctPred ct)
103+ isEmptySetType t1
104+ isEmptySetType t2
105+ return ((EvCoercion $ TcRefl Nominal t1, ct), t1))
106+ in
107+ case x of
108+ Just (ct, tcsA) -> do xs' <- (findSetEquality xs)
109+ tcPluginTrace "SET" $ ppr $ tcsA
110+ tcPluginTrace "SET" $ text $ show tcsA
111+ return $ ct : xs'
112+ Nothing -> findSetEquality xs
113+
114+pluginStop :: () -> TcPluginM ()
115+pluginStop _ = return ()