@@ -1,5 +1,5 @@
11-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2−{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving #-}
2+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators #-}
33
44module TySet(plugin, Set, Union) where
55
@@ -49,6 +49,11 @@ data Set (a :: [k])
4949{- Union operation -}
5050type family Union (a :: [k]) (b :: [k]) :: [k]
5151
52+type family Member (a :: k) (b :: [k]) :: Bool where
53+ Member x '[] = False
54+ Member x (x ': xs) = True
55+ Member x (y ': xs) = Member x xs
56+
5257{- Plugin setup -}
5358plugin :: Plugin
5459plugin = defaultPlugin { tcPlugin = Just . thePlugin }
@@ -94,6 +99,41 @@ isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
9499 guard $ (getOccString . tyConName $ con) == "[]"
95100 _ -> Nothing
96101
102+getNameStr = getOccString . tyConName
103+
104+isUnion :: Type -> Bool
105+isUnion t = case splitTyConApp_maybe t of
106+ Just (x, tcs) -> (getOccString . tyConName $ x) == "Union"
107+ _ -> False
108+
109+-- splitUnion :: Type -> ([Type], [Type])
110+splitUnion t = do (x, tcs) <- splitTyConApp_maybe t
111+ guard $ (getOccString . tyConName $ x) == "Union"
112+
113+splitList t = do (tcon, args) <- splitTyConApp_maybe t
114+ case getNameStr tcon of
115+ ":" -> do guard $ (length args >= 2)
116+ (t1 : (t2 : ts)) <- return args
117+ (kind, emptyArgs) <- splitTyConApp_maybe $ t1
118+ guard $ emptyArgs == []
119+ -- maybe be unnecessary and even restrictive
120+ guard $ getNameStr kind == "*"
121+ ts' <- splitList ts
122+ return $ (t2 : ts')
123+ "[]" -> do guard $ (length args == 1)
124+ [t] <- return args
125+ (kind, emptyArgs) <- splitTyConApp_maybe $ t
126+ -- maybe be unnecessary and even restrictive
127+ guard $ getNameStr kind == "*"
128+ guard $ emptyArgs == []
129+ return $ []
130+ _ -> Nothing
131+
132+unionSingle t = do (x, tcs) <- splitTyConApp_maybe t
133+ guard $ length tcs == 2
134+ guard $ getName x == "Set"
135+ return ()
136+
97137{- Experimenting, finds Set '[] ~ Set '[] and returns a refl coercion
98138 This was set up before when 'Set' was a type family, but is now redundant
99139-}
@@ -103,13 +143,19 @@ findSetEquality (ct : xs) = let x = (do (Nominal,t1,t2) <- getEqPredTys_maybe (c
103143 isEmptySetType t1
104144 isEmptySetType t2
105145 return ((EvCoercion $ TcRefl Nominal t1, ct), t1))
146+ y = do (Nominal,t1,t2) <- getEqPredTys_maybe (ctPred ct)
147+ return t1
106148 in
107149 case x of
108150 Just (ct, tcsA) -> do xs' <- (findSetEquality xs)
109151 tcPluginTrace "SET" $ ppr $ tcsA
110152 tcPluginTrace "SET" $ text $ show tcsA
111153 return $ ct : xs'
112− Nothing -> findSetEquality xs
154+ Nothing -> case y of
155+ Just t -> do tcPluginTrace "SET" $ text $ show t
156+ return []
157+
158+ Nothing -> findSetEquality xs
113159
114160pluginStop :: () -> TcPluginM ()
115161pluginStop _ = return ()