git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Merge pull request #863 from purescript/642

Allow rows in instance contexts

commitd683d32aa8ed1cea30354d337bff7d9fac4bb3d6 authorPhil Freeman <paf31@cantab.net> dateWed 11 Feb 2015, 12:18 (12 years ago) parent7b5cb4b55388ba
4 files changed+71−3
compare with golang
unifiedsplit
examples/passing/RowPolyInstanceContext.purs+20 examples/passing/UnknownInInstance.purs+8 src/Language/PureScript/TypeChecker/Entailment.hs+26−3 src/Language/PureScript/TypeChecker/Unify.hs+17
examples/passing/RowPolyInstanceContext.pursnew file+20
@@ -0,0 +1,20 @@
1+module Main where
2+
3+class T s m where
4+ state :: (s -> s) -> m Unit
5+
6+data S s a = S (s -> { new :: s, ret :: a })
7+
8+instance st :: T s (S s) where
9+ state f = S $ \s -> { new: f s, ret: unit }
10+
11+test1 :: forall r . S { foo :: String | r } Unit
12+test1 = state $ \o -> o { foo = o.foo ++ "!" }
13+
14+test2 :: forall m r . (T { foo :: String | r } m) => m Unit
15+test2 = state $ \o -> o { foo = o.foo ++ "!" }
16+
17+main = do
18+ let t1 = test1
19+ let t2 = test2
20+ Debug.Trace.trace "Done"
examples/passing/UnknownInInstance.pursnew file+8
@@ -0,0 +1,8 @@
1+module Main where
2+
3+data Proxy a = Proxy
4+
5+test :: forall a. (Show (Proxy a)) => String
6+test = show Proxy
7+
8+main = Debug.Trace.trace "Done"
src/Language/PureScript/TypeChecker/Entailment.hs+26−3
@@ -20,6 +20,7 @@ module Language.PureScript.TypeChecker.Entailment (
2020import Data.Function (on)
2121import Data.List
2222import Data.Maybe (maybeToList)
23+import Data.Foldable (foldMap)
2324import qualified Data.Map as M
2425
2526import Control.Applicative
@@ -199,13 +200,35 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt
199200-- and return a substitution from type variables to types which makes the type heads unify.
200201--
201202typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
202−typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
203−typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
203+typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
204+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
205+-- In this case, we might want type information to flow back to the typechecker.
206+-- TODO: run this function in the UnifyT monad.
207+typeHeadsAreEqual _ _ (TUnknown _) _ = Just []
204208typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
205−typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
209+typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2
210+ <*> typeHeadsAreEqual m e t1 t2
206211typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
207212 Left _ -> Nothing
208213 Right t1 -> typeHeadsAreEqual m e t1 t2
214+typeHeadsAreEqual _ _ REmpty REmpty = Just []
215+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
216+ let (s1, r1') = rowToList r1
217+ (s2, r2') = rowToList r2
218+
219+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
220+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
221+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
222+ in (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int
223+ <*> go sd1 r1' sd2 r2'
224+ where
225+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
226+ go [] REmpty [] REmpty = Just []
227+ go [] (TUnknown _) _ _ = Just []
228+ go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
229+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
230+ go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]
231+ go _ _ _ _ = Nothing
209232typeHeadsAreEqual _ _ _ _ = Nothing
210233
211234-- |
src/Language/PureScript/TypeChecker/Unify.hs+17
@@ -153,6 +153,23 @@ unifiesWith e (SaturatedTypeSynonym name args) t2 =
153153 Left _ -> False
154154 Right t1 -> unifiesWith e t1 t2
155155unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
156+unifiesWith _ REmpty REmpty = True
157+unifiesWith e r1@(RCons _ _ _) r2@(RCons _ _ _) =
158+ let (s1, r1') = rowToList r1
159+ (s2, r2') = rowToList r2
160+
161+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
162+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
163+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
164+ in all (\(t1, t2) -> unifiesWith e t1 t2) int && go sd1 r1' sd2 r2'
165+ where
166+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
167+ go [] REmpty [] REmpty = True
168+ go [] (TypeVar v1) [] (TypeVar v2) = v1 == v2
169+ go [] (Skolem _ s1 _) [] (Skolem _ s2 _) = s1 == s2
170+ go _ (TUnknown _) _ _ = True
171+ go _ _ _ (TUnknown _) = True
172+ go _ _ _ _ = False
156173unifiesWith _ _ _ = False
157174
158175-- |