git.iko.soy/rowtype-yoga/purescript-native
on golang help sign in
Functional Dependencies (#2279)

* Unify types which instance heads force to be equal * More * Strict generalization for now * Loop until fixed point * Stream example * Fix test * Remove unused function argument * Add syntax for functional dependencies * More work on fundeps: * Some refactoring * Store functional dependencies in Environment * Add a (currently breaking) test for fundeps * Coverage condition * Dunzo. More tests * Error messages * Better errors * Fix test * It is complete * Remove errors for fundeps * Fix overlapping instances issue * ... * Tidying * use Map * more tidying * Substitution should take account of types which didn't match exactly * Finally done, add @LiamGoodacre's tests * okay ... * GHC.Generics example * Improved generics example * Get rid of the InstanceContext stuff, it was causing problems with defered constraints. Add test case * Fix a warning * D'oh * Various: 1. Allow wildcards in constraints and show the right inferred type 2. Allow ambiguous types in inferred contexts if they can be solved by some functional dependency 3. Some tidying in the TypeChecker.Monad module. * Fix warning in GHC 8 * Improved constraint simplifier * Fix issue with rows in unification check * Fix a small bug in pretty printing * Only require repeated types to be equal on the solved set

commit8197c06483c3d630ac2a22829aaa9b7ebe8a4701 authorPhil Freeman <paf31@cantab.net> dateWed 21 Sep 2016, 09:57 (10 years ago) parentfc8697a
40 files changed+977−454
compare with golang
unifiedsplit
examples/failing/OverlappingVars.purs−1 examples/failing/UnifyInTypeInstanceLookup.purs−22 examples/passing/FunWithFunDeps.js+32 examples/passing/FunWithFunDeps.purs+41 examples/passing/FunctionalDependencies.purs+21 examples/passing/GHCGenerics.purs+140 examples/passing/NewtypeClass.purs+39 examples/passing/RowPolyInstanceContext.purs+1−1 examples/passing/Stream.purs+26 examples/passing/UnifyInTypeInstanceLookup.purs+25 examples/passing/WildcardInInstance.purs+23 hierarchy/Main.hs+2−2 psc-docs/Tags.hs+1−1 src/Control/Monad/Supply/Class.hs+4 src/Language/PureScript/AST/Declarations.hs+1−1 src/Language/PureScript/AST/Exported.hs+1−1 src/Language/PureScript/AST/Traversals.hs+8−8 src/Language/PureScript/CoreFn/Desugar.hs+1−1 src/Language/PureScript/Docs/Convert/Single.hs+2−2 src/Language/PureScript/Environment.hs+40−28 src/Language/PureScript/Errors.hs+11−11 src/Language/PureScript/Externs.hs+27−26 src/Language/PureScript/Ide/SourceFile.hs+1−1 src/Language/PureScript/Interactive/Completion.hs+1−1 src/Language/PureScript/Interactive/Printer.hs+10−10 src/Language/PureScript/Parser/Declarations.hs+6−1 src/Language/PureScript/Parser/Lexer.hs+7 src/Language/PureScript/Pretty/Types.hs+1−1 src/Language/PureScript/Sugar/Names.hs+2−2 src/Language/PureScript/Sugar/Names/Exports.hs+1−1 src/Language/PureScript/Sugar/Operators.hs+2−2 src/Language/PureScript/Sugar/TypeClasses.hs+19−16 src/Language/PureScript/TypeChecker.hs+17−9 src/Language/PureScript/TypeChecker/Entailment.hs+355−148 src/Language/PureScript/TypeChecker/Kinds.hs+7−8 src/Language/PureScript/TypeChecker/Monad.hs+30−18 src/Language/PureScript/TypeChecker/Types.hs+69−75 src/Language/PureScript/TypeChecker/Unify.hs+1−31 src/Language/PureScript/TypeClassDictionaries.hs−23 tests/Language/PureScript/Ide/SourceFileSpec.hs+2−2
examples/failing/OverlappingVars.purs−1
@@ -12,4 +12,3 @@ instance overlappingVarsFoo :: OverlappingVars (Foo a a) where
1212 f a = a
1313
1414test = f (Foo "" 0)
15−
examples/failing/UnifyInTypeInstanceLookup.pursdeleted−22
@@ -1,22 +0,0 @@
1−-- @shouldFailWith NoInstanceFound
2−-- See issue #390.
3−-- TODO: Improve this error.
4−module Main where
5−
6−import Prelude
7−
8−data Z = Z
9−data S n = S n
10−
11−data T
12−data F
13−
14−class EQ x y b
15−instance eqT :: EQ x x T
16−instance eqF :: EQ x y F
17−
18−foreign import test :: forall a b. (EQ a b T) => a -> b -> a
19−
20−foreign import anyNat :: forall a. a
21−
22−test1 = test anyNat (S Z)
examples/passing/FunWithFunDeps.jsnew file+32
@@ -0,0 +1,32 @@
1+
2+//: forall e. FVect Z e
3+exports.fnil = [];
4+
5+//: forall n e. e -> FVect n e -> FVect (S n) e
6+exports.fcons = function (hd) {
7+ return function (tl) {
8+ return [hd].concat(tl);
9+ };
10+};
11+
12+exports.fappend = function (dict) {
13+ return function (left) {
14+ return function (right) {
15+ return left.concat(right);
16+ };
17+ };
18+};
19+
20+exports.fflatten = function (dict) {
21+ return function (v) {
22+ var accRef = [];
23+ for (var indexRef = 0; indexRef < v.length; indexRef += 1) {
24+ accRef = accRef.concat(v[indexRef]);
25+ }
26+ return accRef;
27+ };
28+};
29+
30+exports.ftoArray = function (vect) {
31+ return vect;
32+};
examples/passing/FunWithFunDeps.pursnew file+41
@@ -0,0 +1,41 @@
1+-- Taken from https://github.com/LiamGoodacre/purescript-fun-with-fundeps
2+
3+module Main where
4+
5+import Control.Monad.Eff.Console (log)
6+
7+-- Nat : Type
8+data Z
9+data S n
10+
11+type S2 n = S (S n)
12+type S3 n = S (S2 n)
13+type S4 n = S (S3 n)
14+type S5 n = S (S4 n)
15+type S15 n = S5 (S5 (S5 n))
16+
17+class NatPlus l r o | l r -> o
18+instance natPlusZ :: NatPlus Z r r
19+instance natPlusS :: (NatPlus l r o) => NatPlus (S l) r (S o)
20+
21+class NatMult l r o | l r -> o
22+instance natMultZ :: NatMult Z n Z
23+instance natMultS :: (NatMult m n r, NatPlus n r s) => NatMult (S m) n s
24+
25+-- Foreign Vect
26+foreign import data FVect :: * -> * -> *
27+foreign import fnil :: forall e. FVect Z e
28+foreign import fcons :: forall n e. e -> FVect n e -> FVect (S n) e
29+foreign import fappend :: forall l r o e. (NatPlus l r o) => FVect l e -> FVect r e -> FVect o e
30+foreign import fflatten :: forall f s t o. (NatMult f s o) => FVect f (FVect s t) -> FVect o t
31+foreign import ftoArray :: forall n e. FVect n e -> Array e
32+
33+-- should be able to figure these out
34+fsingleton x = fcons x fnil
35+fexample = fcons 1 (fsingleton 2) `fappend` fsingleton 3 `fappend` fcons 4 (fsingleton 5)
36+fexample2 = fexample `fappend` fexample `fappend` fexample
37+fexample3 = fsingleton fexample `fappend` fsingleton fexample `fappend` fsingleton fexample
38+
39+fexample4 = fflatten fexample3
40+
41+main = log "Done"
examples/passing/FunctionalDependencies.pursnew file+21
@@ -0,0 +1,21 @@
1+module Main where
2+
3+import Control.Monad.Eff.Console (log)
4+
5+data Nil
6+data Cons x xs
7+
8+class Append a b c | a b -> c
9+
10+instance appendNil :: Append Nil b b
11+
12+instance appendCons :: Append xs b c => Append (Cons x xs) b (Cons x c)
13+
14+data Proxy a = Proxy
15+
16+appendProxy :: forall a b c. Append a b c => Proxy a -> Proxy b -> Proxy c
17+appendProxy Proxy Proxy = Proxy
18+
19+test = appendProxy (Proxy :: Proxy (Cons Int Nil)) (Proxy :: Proxy (Cons String Nil))
20+
21+main = log "Done"
examples/passing/GHCGenerics.pursnew file+140
@@ -0,0 +1,140 @@
1+-- An example to show how we could implement GHC-style Generics using
2+-- functional dependencies.
3+--
4+-- See https://hackage.haskell.org/package/base-4.9.0.0/docs/GHC-Generics.html
5+
6+module Main where
7+
8+import Prelude
9+import Control.Monad.Eff (Eff)
10+import Control.Monad.Eff.Console (CONSOLE, log, logShow)
11+
12+-- Representation for types with no constructors
13+data V1
14+
15+-- Representation for constructors with no arguments
16+data U1 = U1
17+
18+-- Representation for sum types
19+data Sum a b = Inl a | Inr b
20+
21+infixr 5 type Sum as +
22+
23+-- Representation for product types
24+data Product a b = Product a b
25+
26+infixr 6 type Product as *
27+
28+-- Representation for data constructors, with the data constructor name indicated
29+-- at the type level.
30+data Ctor (name :: Symbol) a = Ctor a
31+
32+-- Representation for occurrences of other types in a data type definition.
33+data K a = K a
34+
35+-- The Generic class asserts the existence of a type function from "real" types
36+-- to representation types, and an isomorphism between them.
37+class Generic a repr | a -> repr where
38+ to :: a -> repr
39+ from :: repr -> a
40+
41+-- We can write an instance for the (recursive) type of lists. Note that these
42+-- instances would be generated by the compiler ideally.
43+data List a = Nil | Cons a (List a)
44+
45+instance genericList :: Generic (List a) (Ctor "Nil" U1 + Ctor "Cons" (K a * K (List a))) where
46+ to Nil = Inl (Ctor U1)
47+ to (Cons x xs) = Inr (Ctor (Product (K x) (K xs)))
48+ from (Inl (Ctor U1)) = Nil
49+ from (Inr (Ctor (Product (K x) (K xs)))) = Cons x xs
50+
51+-- We'd like to refect type level strings (for data constructor names) at the value
52+-- level, so that we can "show" them. Again, these instances would ideally be derived
53+-- for us.
54+class KnownSymbol (sym :: Symbol) where
55+ symbol :: forall proxy. proxy sym -> String
56+
57+instance knownSymbolNil :: KnownSymbol "Nil" where
58+ symbol _ = "Nil"
59+
60+instance knownSymbolCons :: KnownSymbol "Cons" where
61+ symbol _ = "Cons"
62+
63+-- A proxy for a type-level string.
64+data SProxy (sym :: Symbol) = SProxy
65+
66+-- To write generic functions, we create a corresponding type class, and use the
67+-- type class machinery to infer the correct function based on the representation
68+-- type.
69+class GShow a where
70+ gShow :: a -> String
71+
72+-- Now provide instances for GShow for the appropriate representation types.
73+-- Note: we don't have to implement all instances here.
74+
75+instance gShowU1 :: GShow U1 where
76+ gShow _ = ""
77+
78+instance gShowSum :: (GShow a, GShow b) => GShow (a + b) where
79+ gShow (Inl a) = gShow a
80+ gShow (Inr b) = gShow b
81+
82+instance gShowProduct :: (GShow a, GShow b) => GShow (a * b) where
83+ gShow (Product a b) = gShow a <> gShow b
84+
85+instance gShowCtor :: (KnownSymbol ctor, GShow a) => GShow (Ctor ctor a) where
86+ gShow (Ctor a) = "(" <> symbol (SProxy :: SProxy ctor) <> gShow a <> ")"
87+
88+instance gShowK :: Show a => GShow (K a) where
89+ gShow (K a) = " " <> show a
90+
91+-- Now we can implement a generic show function which uses the GShow instance
92+-- on the representation type.
93+genericShow :: forall a repr. (Generic a repr, GShow repr) => a -> String
94+genericShow x = gShow (to x)
95+
96+-- Note how the required instance here is Show a, and not Generic a.
97+-- This allows us to use generic programming on a wider variety of types
98+-- (including types which contain foreign types) than we can use now.
99+instance showList :: Show a => Show (List a) where
100+ show xs = genericShow xs -- (we need to eta expand here to avoid stack overflow
101+ -- due to recursion implicit in the instance lookup)
102+
103+-- Another example: Eq
104+
105+class GEq a where
106+ gEq :: a -> a -> Boolean
107+
108+instance gEqU1 :: GEq U1 where
109+ gEq _ _ = true
110+
111+instance gEqSum :: (GEq a, GEq b) => GEq (a + b) where
112+ gEq (Inl a1) (Inl a2) = gEq a1 a2
113+ gEq (Inr b1) (Inr b2) = gEq b1 b2
114+ gEq _ _ = false
115+
116+instance gEqProduct :: (GEq a, GEq b) => GEq (a * b) where
117+ gEq (Product a1 b1) (Product a2 b2) = gEq a1 a2 && gEq b1 b2
118+
119+instance gEqCtor :: (KnownSymbol ctor, GEq a) => GEq (Ctor ctor a) where
120+ gEq (Ctor a1) (Ctor a2) = gEq a1 a2
121+
122+instance gEqK :: Eq a => GEq (K a) where
123+ gEq (K a1) (K a2) = a1 == a2
124+
125+genericEq :: forall a repr. (Generic a repr, GEq repr) => a -> a -> Boolean
126+genericEq x y = gEq (to x) (to y)
127+
128+instance eqList :: Eq a => Eq (List a) where
129+ eq xs ys = genericEq xs ys
130+
131+main :: Eff (console :: CONSOLE) Unit
132+main = do
133+ logShow (Cons 1 Nil)
134+ logShow (Cons 1 (Cons 2 Nil))
135+ logShow (Cons 'x' (Cons 'y' (Cons 'z' Nil)))
136+
137+ logShow (Cons 1 (Cons 2 Nil) == Cons 1 (Cons 2 Nil))
138+ logShow (Cons 1 (Cons 2 Nil) == Cons 1 Nil)
139+
140+ log "Done"
examples/passing/NewtypeClass.pursnew file+39
@@ -0,0 +1,39 @@
1+module Main where
2+
3+import Prelude
4+import Control.Monad.Eff
5+import Control.Monad.Eff.Console
6+
7+class Newtype t a | t -> a where
8+ wrap :: a -> t
9+ unwrap :: t -> a
10+
11+instance newtypeMultiplicative :: Newtype (Multiplicative a) a where
12+ wrap = Multiplicative
13+ unwrap (Multiplicative a) = a
14+
15+data Multiplicative a = Multiplicative a
16+
17+instance semiringMultiplicative :: Semiring a => Semigroup (Multiplicative a) where
18+ append (Multiplicative a) (Multiplicative b) = Multiplicative (a * b)
19+
20+data Pair a = Pair a a
21+
22+foldPair :: forall a s. Semigroup s => (a -> s) -> Pair a -> s
23+foldPair f (Pair a b) = f a <> f b
24+
25+ala
26+ :: forall f t a
27+ . (Functor f, Newtype t a)
28+ => (a -> t)
29+ -> ((a -> t) -> f t)
30+ -> f a
31+ala _ f = map unwrap (f wrap)
32+
33+test = ala Multiplicative foldPair
34+
35+test1 = ala Multiplicative foldPair (Pair 2 3)
36+
37+main = do
38+ logShow (test (Pair 2 3))
39+ log "Done"
examples/passing/RowPolyInstanceContext.purs+1−1
@@ -3,7 +3,7 @@ module Main where
33import Prelude
44import Control.Monad.Eff.Console (log)
55
6−class T s m where
6+class T s m | m -> s where
77 state :: (s -> s) -> m Unit
88
99data S s a = S (s -> { new :: s, ret :: a })
examples/passing/Stream.pursnew file+26
@@ -0,0 +1,26 @@
1+module Main where
2+
3+import Prelude
4+
5+import Control.Monad.Eff (Eff)
6+import Control.Monad.Eff.Console (CONSOLE, log)
7+
8+class IsStream el s | s -> el where
9+ cons :: el -> (Unit -> s) -> s
10+ uncons :: s -> { head :: el, tail :: s }
11+
12+data Stream a = Stream a (Unit -> Stream a)
13+
14+instance streamIsStream :: IsStream a (Stream a) where
15+ cons x xs = Stream x xs
16+ uncons (Stream x f) = { head: x, tail: f unit }
17+
18+test :: forall el s. IsStream el s => s -> s
19+test s = case uncons s of
20+ { head, tail } -> cons head \_ -> tail
21+
22+main :: Eff (console :: CONSOLE) Unit
23+main = do
24+ let dones :: Stream String
25+ dones = cons "Done" \_ -> dones
26+ log (uncons (test dones)).head
examples/passing/UnifyInTypeInstanceLookup.pursnew file+25
@@ -0,0 +1,25 @@
1+module Main where
2+
3+import Control.Monad.Eff.Console (log)
4+
5+data Z = Z
6+data S n = S n
7+
8+data T
9+data F
10+
11+class EQ x y b
12+instance eqT :: EQ x x T
13+instance eqF :: EQ x y F
14+
15+test :: forall a b. (EQ a b T) => a -> b -> a
16+test a _ = a
17+
18+spin :: forall a b. a -> b
19+spin a = spin a
20+
21+-- Expected type:
22+-- forall t. (EQ t (S Z) T) => t
23+test1 = test (spin 1) (S Z)
24+
25+main = log "Done"
examples/passing/WildcardInInstance.pursnew file+23
@@ -0,0 +1,23 @@
1+module Main where
2+
3+import Prelude
4+import Control.Monad.Eff
5+import Control.Monad.Eff.Console
6+
7+-- Until the functional dependency gets added to purescript-eff,
8+-- we need this here.
9+class Monad m <= MonadEff eff m | m -> eff where
10+ liftEff :: forall a. Eff eff a -> m a
11+
12+instance monadEffEff :: MonadEff eff (Eff eff) where
13+ liftEff = id
14+
15+-- This should generate a warning with the correct inferred type.
16+test :: forall m. MonadEff _ m => m Unit
17+test = liftEff $ log "Done"
18+
19+test1 :: Eff _ Unit
20+test1 = liftEff $ log "Done"
21+
22+main :: forall eff. Eff (console :: CONSOLE | eff) Unit
23+main = test
hierarchy/Main.hs+2−2
@@ -86,9 +86,9 @@ compile (HierarchyOptions inputGlob mOutput) = do
8686 exitSuccess
8787
8888superClasses :: P.Declaration -> [SuperMap]
89−superClasses (P.TypeClassDeclaration sub _ supers@(_:_) _) =
89+superClasses (P.TypeClassDeclaration sub _ supers@(_:_) _ _) =
9090 fmap (\(P.Constraint (P.Qualified _ super) _ _) -> SuperMap (Right (super, sub))) supers
91−superClasses (P.TypeClassDeclaration sub _ _ _) = [SuperMap (Left sub)]
91+superClasses (P.TypeClassDeclaration sub _ _ _ _) = [SuperMap (Left sub)]
9292superClasses (P.PositionedDeclaration _ _ decl) = superClasses decl
9393superClasses _ = []
9494
psc-docs/Tags.hs+1−1
@@ -13,6 +13,6 @@ tags = concatMap dtags . P.exportedDeclarations
1313 names (P.TypeDeclaration ident _) = [P.showIdent ident]
1414 names (P.ExternDeclaration ident _) = [P.showIdent ident]
1515 names (P.TypeSynonymDeclaration name _ _) = [P.runProperName name]
16− names (P.TypeClassDeclaration name _ _ _) = [P.runProperName name]
16+ names (P.TypeClassDeclaration name _ _ _ _) = [P.runProperName name]
1717 names (P.TypeInstanceDeclaration name _ _ _ _) = [P.showIdent name]
1818 names _ = []
src/Control/Monad/Supply/Class.hs+4
@@ -7,6 +7,7 @@ import Prelude.Compat
77
88import Control.Monad.Supply
99import Control.Monad.State
10+import Control.Monad.Writer
1011
1112class Monad m => MonadSupply m where
1213 fresh :: m Integer
@@ -20,5 +21,8 @@ instance Monad m => MonadSupply (SupplyT m) where
2021instance MonadSupply m => MonadSupply (StateT s m) where
2122 fresh = lift fresh
2223
24+instance (Monoid w, MonadSupply m) => MonadSupply (WriterT w m) where
25+ fresh = lift fresh
26+
2327freshName :: MonadSupply m => m String
2428freshName = fmap (('$' :) . show) fresh
src/Language/PureScript/AST/Declarations.hs+1−1
@@ -349,7 +349,7 @@ data Declaration
349349 -- |
350350 -- A type class declaration (name, argument, implies, member declarations)
351351 --
352− | TypeClassDeclaration (ProperName 'ClassName) [(String, Maybe Kind)] [Constraint] [Declaration]
352+ | TypeClassDeclaration (ProperName 'ClassName) [(String, Maybe Kind)] [Constraint] [FunctionalDependency] [Declaration]
353353 -- |
354354 -- A type instance declaration (name, dependencies, class name, instance types, member
355355 -- declarations)
src/Language/PureScript/AST/Exported.hs+1−1
@@ -133,7 +133,7 @@ isExported (Just exps) decl = any (matches decl) exps
133133 matches (DataDeclaration _ ident _ _) (TypeRef ident' _) = ident == ident'
134134 matches (ExternDataDeclaration ident _) (TypeRef ident' _) = ident == ident'
135135 matches (TypeSynonymDeclaration ident _ _) (TypeRef ident' _) = ident == ident'
136− matches (TypeClassDeclaration ident _ _ _) (TypeClassRef ident') = ident == ident'
136+ matches (TypeClassDeclaration ident _ _ _ _) (TypeClassRef ident') = ident == ident'
137137 matches (ValueFixityDeclaration _ _ op) (ValueOpRef op') = op == op'
138138 matches (TypeFixityDeclaration _ _ op) (TypeOpRef op') = op == op'
139139 matches (PositionedDeclaration _ _ d) r = d `matches` r
src/Language/PureScript/AST/Traversals.hs+8−8
@@ -34,7 +34,7 @@ everywhereOnValues f g h = (f', g', h')
3434 f' (DataBindingGroupDeclaration ds) = f (DataBindingGroupDeclaration (map f' ds))
3535 f' (ValueDeclaration name nameKind bs val) = f (ValueDeclaration name nameKind (map h' bs) ((map (g' *** g') +++ g') val))
3636 f' (BindingGroupDeclaration ds) = f (BindingGroupDeclaration (map (\(name, nameKind, val) -> (name, nameKind, g' val)) ds))
37− f' (TypeClassDeclaration name args implies ds) = f (TypeClassDeclaration name args implies (map f' ds))
37+ f' (TypeClassDeclaration name args implies deps ds) = f (TypeClassDeclaration name args implies deps (map f' ds))
3838 f' (TypeInstanceDeclaration name cs className args ds) = f (TypeInstanceDeclaration name cs className args (mapTypeInstanceBody (map f') ds))
3939 f' (PositionedDeclaration pos com d) = f (PositionedDeclaration pos com (f' d))
4040 f' other = f other
@@ -101,7 +101,7 @@ everywhereOnValuesTopDownM f g h = (f' <=< f, g' <=< g, h' <=< h)
101101 f' (DataBindingGroupDeclaration ds) = DataBindingGroupDeclaration <$> traverse (f' <=< f) ds
102102 f' (ValueDeclaration name nameKind bs val) = ValueDeclaration name nameKind <$> traverse (h' <=< h) bs <*> eitherM (traverse (pairM (g' <=< g) (g' <=< g))) (g' <=< g) val
103103 f' (BindingGroupDeclaration ds) = BindingGroupDeclaration <$> traverse (\(name, nameKind, val) -> (,,) name nameKind <$> (g val >>= g')) ds
104− f' (TypeClassDeclaration name args implies ds) = TypeClassDeclaration name args implies <$> traverse (f' <=< f) ds
104+ f' (TypeClassDeclaration name args implies deps ds) = TypeClassDeclaration name args implies deps <$> traverse (f' <=< f) ds
105105 f' (TypeInstanceDeclaration name cs className args ds) = TypeInstanceDeclaration name cs className args <$> traverseTypeInstanceBody (traverse (f' <=< f)) ds
106106 f' (PositionedDeclaration pos com d) = PositionedDeclaration pos com <$> (f d >>= f')
107107 f' other = f other
@@ -168,7 +168,7 @@ everywhereOnValuesM f g h = (f', g', h')
168168 f' (DataBindingGroupDeclaration ds) = (DataBindingGroupDeclaration <$> traverse f' ds) >>= f
169169 f' (ValueDeclaration name nameKind bs val) = (ValueDeclaration name nameKind <$> traverse h' bs <*> eitherM (traverse (pairM g' g')) g' val) >>= f
170170 f' (BindingGroupDeclaration ds) = (BindingGroupDeclaration <$> traverse (\(name, nameKind, val) -> (,,) name nameKind <$> g' val) ds) >>= f
171− f' (TypeClassDeclaration name args implies ds) = (TypeClassDeclaration name args implies <$> traverse f' ds) >>= f
171+ f' (TypeClassDeclaration name args implies deps ds) = (TypeClassDeclaration name args implies deps <$> traverse f' ds) >>= f
172172 f' (TypeInstanceDeclaration name cs className args ds) = (TypeInstanceDeclaration name cs className args <$> traverseTypeInstanceBody (traverse f') ds) >>= f
173173 f' (PositionedDeclaration pos com d) = (PositionedDeclaration pos com <$> f' d) >>= f
174174 f' other = f other
@@ -240,7 +240,7 @@ everythingOnValues (<>) f g h i j = (f', g', h', i', j')
240240 f' d@(ValueDeclaration _ _ bs (Right val)) = foldl (<>) (f d) (map h' bs) <> g' val
241241 f' d@(ValueDeclaration _ _ bs (Left gs)) = foldl (<>) (f d) (map h' bs ++ concatMap (\(grd, val) -> [g' grd, g' val]) gs)
242242 f' d@(BindingGroupDeclaration ds) = foldl (<>) (f d) (map (\(_, _, val) -> g' val) ds)
243− f' d@(TypeClassDeclaration _ _ _ ds) = foldl (<>) (f d) (map f' ds)
243+ f' d@(TypeClassDeclaration _ _ _ _ ds) = foldl (<>) (f d) (map f' ds)
244244 f' d@(TypeInstanceDeclaration _ _ _ _ (ExplicitInstance ds)) = foldl (<>) (f d) (map f' ds)
245245 f' d@(PositionedDeclaration _ _ d1) = f d <> f' d1
246246 f' d = f d
@@ -314,7 +314,7 @@ everythingWithContextOnValues s0 r0 (<>) f g h i j = (f'' s0, g'' s0, h'' s0, i'
314314 f' s (ValueDeclaration _ _ bs (Right val)) = foldl (<>) r0 (map (h'' s) bs) <> g'' s val
315315 f' s (ValueDeclaration _ _ bs (Left gs)) = foldl (<>) r0 (map (h'' s) bs ++ concatMap (\(grd, val) -> [g'' s grd, g'' s val]) gs)
316316 f' s (BindingGroupDeclaration ds) = foldl (<>) r0 (map (\(_, _, val) -> g'' s val) ds)
317− f' s (TypeClassDeclaration _ _ _ ds) = foldl (<>) r0 (map (f'' s) ds)
317+ f' s (TypeClassDeclaration _ _ _ _ ds) = foldl (<>) r0 (map (f'' s) ds)
318318 f' s (TypeInstanceDeclaration _ _ _ _ (ExplicitInstance ds)) = foldl (<>) r0 (map (f'' s) ds)
319319 f' s (PositionedDeclaration _ _ d1) = f'' s d1
320320 f' _ _ = r0
@@ -395,7 +395,7 @@ everywhereWithContextOnValuesM s0 f g h i j = (f'' s0, g'' s0, h'' s0, i'' s0, j
395395 f' s (DataBindingGroupDeclaration ds) = DataBindingGroupDeclaration <$> traverse (f'' s) ds
396396 f' s (ValueDeclaration name nameKind bs val) = ValueDeclaration name nameKind <$> traverse (h'' s) bs <*> eitherM (traverse (pairM (g'' s) (g'' s))) (g'' s) val
397397 f' s (BindingGroupDeclaration ds) = BindingGroupDeclaration <$> traverse (thirdM (g'' s)) ds
398− f' s (TypeClassDeclaration name args implies ds) = TypeClassDeclaration name args implies <$> traverse (f'' s) ds
398+ f' s (TypeClassDeclaration name args implies deps ds) = TypeClassDeclaration name args implies deps <$> traverse (f'' s) ds
399399 f' s (TypeInstanceDeclaration name cs className args ds) = TypeInstanceDeclaration name cs className args <$> traverseTypeInstanceBody (traverse (f'' s)) ds
400400 f' s (PositionedDeclaration pos com d1) = PositionedDeclaration pos com <$> f'' s d1
401401 f' _ other = return other
@@ -482,7 +482,7 @@ everythingWithScope f g h i j = (f'', g'', h'', i'', \s -> snd . j'' s)
482482 f' s (BindingGroupDeclaration ds) =
483483 let s' = S.union s (S.fromList (map (\(name, _, _) -> name) ds))
484484 in foldMap (\(_, _, val) -> g'' s' val) ds
485− f' s (TypeClassDeclaration _ _ _ ds) = foldMap (f'' s) ds
485+ f' s (TypeClassDeclaration _ _ _ _ ds) = foldMap (f'' s) ds
486486 f' s (TypeInstanceDeclaration _ _ _ _ (ExplicitInstance ds)) = foldMap (f'' s) ds
487487 f' s (PositionedDeclaration _ _ d) = f'' s d
488488 f' _ _ = mempty
@@ -576,7 +576,7 @@ accumTypes f = everythingOnValues mappend forDecls forValues (const mempty) (con
576576 where
577577 forDecls (DataDeclaration _ _ _ dctors) = mconcat (concatMap (map f . snd) dctors)
578578 forDecls (ExternDeclaration _ ty) = f ty
579− forDecls (TypeClassDeclaration _ _ implies _) = mconcat (concatMap (map f . constraintArgs) implies)
579+ forDecls (TypeClassDeclaration _ _ implies _ _) = mconcat (concatMap (map f . constraintArgs) implies)
580580 forDecls (TypeInstanceDeclaration _ cs _ tys _) = mconcat (concatMap (map f . constraintArgs) cs) `mappend` mconcat (map f tys)
581581 forDecls (TypeSynonymDeclaration _ _ ty) = f ty
582582 forDecls (TypeDeclaration _ ty) = f ty
src/Language/PureScript/CoreFn/Desugar.hs+1−1
@@ -72,7 +72,7 @@ moduleToCoreFn env (A.Module _ coms mn decls (Just exps)) =
7272 [NonRec (ssA ss) name (exprToCoreFn ss com Nothing e)]
7373 declToCoreFn ss _ (A.BindingGroupDeclaration ds) =
7474 [Rec $ map (\(name, _, e) -> ((ssA ss, name), exprToCoreFn ss [] Nothing e)) ds]
75− declToCoreFn ss com (A.TypeClassDeclaration name _ supers members) =
75+ declToCoreFn ss com (A.TypeClassDeclaration name _ supers _ members) =
7676 [NonRec (ssA ss) (properToIdent name) $ mkTypeClassConstructor ss com supers members]
7777 declToCoreFn _ com (A.PositionedDeclaration ss com1 d) =
7878 declToCoreFn (Just ss) (com ++ com1) d
src/Language/PureScript/Docs/Convert/Single.hs+2−2
@@ -81,7 +81,7 @@ getDeclarationTitle (P.ExternDeclaration name _) = Just (P.showIdent name)
8181getDeclarationTitle (P.DataDeclaration _ name _ _) = Just (P.runProperName name)
8282getDeclarationTitle (P.ExternDataDeclaration name _) = Just (P.runProperName name)
8383getDeclarationTitle (P.TypeSynonymDeclaration name _ _) = Just (P.runProperName name)
84−getDeclarationTitle (P.TypeClassDeclaration name _ _ _) = Just (P.runProperName name)
84+getDeclarationTitle (P.TypeClassDeclaration name _ _ _ _) = Just (P.runProperName name)
8585getDeclarationTitle (P.TypeInstanceDeclaration name _ _ _ _) = Just (P.showIdent name)
8686getDeclarationTitle (P.TypeFixityDeclaration _ _ op) = Just ("type " ++ P.showOp op)
8787getDeclarationTitle (P.ValueFixityDeclaration _ _ op) = Just (P.showOp op)
@@ -121,7 +121,7 @@ convertDeclaration (P.ExternDataDeclaration _ kind') title =
121121 basicDeclaration title (ExternDataDeclaration kind')
122122convertDeclaration (P.TypeSynonymDeclaration _ args ty) title =
123123 basicDeclaration title (TypeSynonymDeclaration args ty)
124−convertDeclaration (P.TypeClassDeclaration _ args implies ds) title =
124+convertDeclaration (P.TypeClassDeclaration _ args implies _ ds) title = -- TODO: include fundep info
125125 Just (Right (mkDeclaration title info) { declChildren = children })
126126 where
127127 info = TypeClassDeclaration args implies
src/Language/PureScript/Environment.hs+40−28
@@ -18,35 +18,46 @@ import Language.PureScript.TypeClassDictionaries
1818import Language.PureScript.Types
1919import qualified Language.PureScript.Constants as C
2020
21−-- |
22−-- The @Environment@ defines all values and types which are currently in scope:
23−--
24−data Environment = Environment {
25− -- |
26− -- Value names currently in scope
27− --
28− names :: M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
29− -- |
30− -- Type names currently in scope
31− --
21+-- | The @Environment@ defines all values and types which are currently in scope:
22+data Environment = Environment
23+ { names :: M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
24+ -- ^ Values currently in scope
3225 , types :: M.Map (Qualified (ProperName 'TypeName)) (Kind, TypeKind)
33− -- |
34− -- Data constructors currently in scope, along with their associated type
35− -- constructor name, argument types and return type.
26+ -- ^ Type names currently in scope
3627 , dataConstructors :: M.Map (Qualified (ProperName 'ConstructorName)) (DataDeclType, ProperName 'TypeName, Type, [Ident])
37− -- |
38− -- Type synonyms currently in scope
39− --
28+ -- ^ Data constructors currently in scope, along with their associated type
29+ -- constructor name, argument types and return type.
4030 , typeSynonyms :: M.Map (Qualified (ProperName 'TypeName)) ([(String, Maybe Kind)], Type)
41− -- |
42− -- Available type class dictionaries
43− --
31+ -- ^ Type synonyms currently in scope
4432 , typeClassDictionaries :: M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
45− -- |
46− -- Type classes
47− --
48− , typeClasses :: M.Map (Qualified (ProperName 'ClassName)) ([(String, Maybe Kind)], [(Ident, Type)], [Constraint])
49− } deriving (Show)
33+ -- ^ Available type class dictionaries
34+ , typeClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
35+ -- ^ Type classes
36+ } deriving Show
37+
38+-- | Information about a type class
39+data TypeClassData = TypeClassData
40+ { typeClassArguments :: [(String, Maybe Kind)]
41+ -- ^ A list of type argument names, and their kinds, where kind annotations
42+ -- were provided.
43+ , typeClassMembers :: [(Ident, Type)]
44+ -- ^ A list of type class members and their types. Type arguments listed above
45+ -- are considered bound in these types.
46+ , typeClassSuperclasses :: [Constraint]
47+ -- ^ A list of superclasses of this type class. Type arguments listed above
48+ -- are considered bound in the types appearing in these constraints.
49+ , typeClassDependencies :: [FunctionalDependency]
50+ -- ^ A list of functional dependencies for the type arguments of this class.
51+ } deriving Show
52+
53+-- | A functional dependency indicates a relationship between two sets of
54+-- type arguments in a class declaration.
55+data FunctionalDependency = FunctionalDependency
56+ { fdDeterminers :: [Int]
57+ -- ^ the type arguments which determine the determined type arguments
58+ , fdDetermined :: [Int]
59+ -- ^ the determined type arguments
60+ } deriving Show
5061
5162-- |
5263-- The initial environment with no values and only the default javascript types defined
@@ -249,11 +260,11 @@ primTypes =
249260-- The primitive class map. This just contains to `Partial` class, used as a
250261-- kind of magic constraint for partial functions.
251262--
252−primClasses :: M.Map (Qualified (ProperName 'ClassName)) ([(String, Maybe Kind)], [(Ident, Type)], [Constraint])
263+primClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
253264primClasses =
254265 M.fromList
255− [ (primName "Partial", ([], [], []))
256− , (primName "Fail", ([("message", Just Symbol)], [], []))
266+ [ (primName "Partial", (TypeClassData [] [] [] []))
267+ , (primName "Fail", (TypeClassData [("message", Just Symbol)] [] [] []))
257268 ]
258269
259270-- |
@@ -278,3 +289,4 @@ lookupValue :: Environment -> Qualified Ident -> Maybe (Type, NameKind, NameVisi
278289lookupValue env ident = ident `M.lookup` names env
279290
280291$(deriveJSON (defaultOptions { sumEncoding = ObjectWithSingleField }) ''TypeKind)
292+$(deriveJSON (defaultOptions { sumEncoding = ObjectWithSingleField }) ''FunctionalDependency)
src/Language/PureScript/Errors.hs+11−11
@@ -953,7 +953,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS
953953 ]
954954 renderHint (ErrorSolvingConstraint (Constraint nm ts _)) detail =
955955 paras [ detail
956− , line "while solving type class constriant"
956+ , line "while solving type class constraint"
957957 , markCodeBox $ indent $ Box.hsep 1 Box.left
958958 [ line (showQualified runProperName nm)
959959 , Box.vcat Box.left (map typeAtomAsBox ts)
@@ -1063,16 +1063,16 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS
10631063 stripFirst _ [] = []
10641064
10651065 hintCategory :: ErrorMessageHint -> HintCategory
1066− hintCategory ErrorCheckingType{} = ExprHint
1067− hintCategory ErrorInferringType{} = ExprHint
1068− hintCategory ErrorInExpression{} = ExprHint
1069− hintCategory ErrorUnifyingTypes{} = CheckHint
1070− hintCategory ErrorInSubsumption{} = CheckHint
1071− hintCategory ErrorInApplication{} = CheckHint
1072− hintCategory ErrorCheckingKind{} = CheckHint
1073− hintCategory ErrorSolvingConstraint{} = SolverHint
1074− hintCategory PositionedError{} = PositionHint
1075− hintCategory _ = OtherHint
1066+ hintCategory ErrorCheckingType{} = ExprHint
1067+ hintCategory ErrorInferringType{} = ExprHint
1068+ hintCategory ErrorInExpression{} = ExprHint
1069+ hintCategory ErrorUnifyingTypes{} = CheckHint
1070+ hintCategory ErrorInSubsumption{} = CheckHint
1071+ hintCategory ErrorInApplication{} = CheckHint
1072+ hintCategory ErrorCheckingKind{} = CheckHint
1073+ hintCategory ErrorSolvingConstraint{} = SolverHint
1074+ hintCategory PositionedError{} = PositionHint
1075+ hintCategory _ = OtherHint
10761076
10771077-- Pretty print and export declaration
10781078prettyPrintExport :: DeclarationRef -> String
src/Language/PureScript/Externs.hs+27−26
@@ -93,44 +93,45 @@ data ExternsTypeFixity = ExternsTypeFixity
9393data ExternsDeclaration =
9494 -- | A type declaration
9595 EDType
96− { edTypeName :: ProperName 'TypeName
97− , edTypeKind :: Kind
98− , edTypeDeclarationKind :: TypeKind
96+ { edTypeName :: ProperName 'TypeName
97+ , edTypeKind :: Kind
98+ , edTypeDeclarationKind :: TypeKind
9999 }
100100 -- | A type synonym
101101 | EDTypeSynonym
102− { edTypeSynonymName :: ProperName 'TypeName
103− , edTypeSynonymArguments :: [(String, Maybe Kind)]
104− , edTypeSynonymType :: Type
102+ { edTypeSynonymName :: ProperName 'TypeName
103+ , edTypeSynonymArguments :: [(String, Maybe Kind)]
104+ , edTypeSynonymType :: Type
105105 }
106106 -- | A data construtor
107107 | EDDataConstructor
108− { edDataCtorName :: ProperName 'ConstructorName
109− , edDataCtorOrigin :: DataDeclType
110− , edDataCtorTypeCtor :: ProperName 'TypeName
111− , edDataCtorType :: Type
112− , edDataCtorFields :: [Ident]
108+ { edDataCtorName :: ProperName 'ConstructorName
109+ , edDataCtorOrigin :: DataDeclType
110+ , edDataCtorTypeCtor :: ProperName 'TypeName
111+ , edDataCtorType :: Type
112+ , edDataCtorFields :: [Ident]
113113 }
114114 -- | A value declaration
115115 | EDValue
116− { edValueName :: Ident
117− , edValueType :: Type
116+ { edValueName :: Ident
117+ , edValueType :: Type
118118 }
119119 -- | A type class declaration
120120 | EDClass
121− { edClassName :: ProperName 'ClassName
122− , edClassTypeArguments :: [(String, Maybe Kind)]
123− , edClassMembers :: [(Ident, Type)]
124− , edClassConstraints :: [Constraint]
121+ { edClassName :: ProperName 'ClassName
122+ , edClassTypeArguments :: [(String, Maybe Kind)]
123+ , edClassMembers :: [(Ident, Type)]
124+ , edClassConstraints :: [Constraint]
125+ , edFunctionalDependencies :: [FunctionalDependency]
125126 }
126127 -- | An instance declaration
127128 | EDInstance
128− { edInstanceClassName :: Qualified (ProperName 'ClassName)
129− , edInstanceName :: Ident
130− , edInstanceTypes :: [Type]
131− , edInstanceConstraints :: Maybe [Constraint]
129+ { edInstanceClassName :: Qualified (ProperName 'ClassName)
130+ , edInstanceName :: Ident
131+ , edInstanceTypes :: [Type]
132+ , edInstanceConstraints :: Maybe [Constraint]
132133 }
133− deriving (Show)
134+ deriving Show
134135
135136-- | Convert an externs file back into a module
136137applyExternsFileToEnvironment :: ExternsFile -> Environment -> Environment
@@ -141,7 +142,7 @@ applyExternsFileToEnvironment ExternsFile{..} = flip (foldl' applyDecl) efDeclar
141142 applyDecl env (EDTypeSynonym pn args ty) = env { typeSynonyms = M.insert (qual pn) (args, ty) (typeSynonyms env) }
142143 applyDecl env (EDDataConstructor pn dTy tNm ty nms) = env { dataConstructors = M.insert (qual pn) (dTy, tNm, ty, nms) (dataConstructors env) }
143144 applyDecl env (EDValue ident ty) = env { names = M.insert (Qualified (Just efModuleName) ident) (ty, External, Defined) (names env) }
144− applyDecl env (EDClass pn args members cs) = env { typeClasses = M.insert (qual pn) (args, members, cs) (typeClasses env) }
145+ applyDecl env (EDClass pn args members cs deps) = env { typeClasses = M.insert (qual pn) (TypeClassData args members cs deps) (typeClasses env) }
145146 applyDecl env (EDInstance className ident tys cs) = env { typeClassDictionaries = updateMap (updateMap (M.insert (qual ident) dict) className) (Just efModuleName) (typeClassDictionaries env) }
146147 where
147148 dict :: TypeClassDictionaryInScope
@@ -204,12 +205,12 @@ moduleToExternsFile (Module _ _ mn ds (Just exps)) env = ExternsFile{..}
204205 | Just (ty, _, _) <- Qualified (Just mn) ident `M.lookup` names env
205206 = [ EDValue ident ty ]
206207 toExternsDeclaration (TypeClassRef className)
207− | Just (args, members, implies) <- Qualified (Just mn) className `M.lookup` typeClasses env
208+ | Just TypeClassData{..} <- Qualified (Just mn) className `M.lookup` typeClasses env
208209 , Just (kind, TypeSynonym) <- Qualified (Just mn) (coerceProperName className) `M.lookup` types env
209210 , Just (_, synTy) <- Qualified (Just mn) (coerceProperName className) `M.lookup` typeSynonyms env
210211 = [ EDType (coerceProperName className) kind TypeSynonym
211− , EDTypeSynonym (coerceProperName className) args synTy
212− , EDClass className args members implies
212+ , EDTypeSynonym (coerceProperName className) typeClassArguments synTy
213+ , EDClass className typeClassArguments typeClassMembers typeClassSuperclasses typeClassDependencies
213214 ]
214215 toExternsDeclaration (TypeInstanceRef ident)
215216 = [ EDInstance tcdClassName ident tcdInstanceTypes tcdDependencies
src/Language/PureScript/Ide/SourceFile.hs+1−1
@@ -104,7 +104,7 @@ extractSpans ss d = case d of
104104 [(Left (runIdentT i), ss)]
105105 P.TypeSynonymDeclaration name _ _ ->
106106 [(Right (runProperNameT name), ss)]
107− P.TypeClassDeclaration name _ _ members ->
107+ P.TypeClassDeclaration name _ _ _ members ->
108108 (Right (runProperNameT name), ss) : concatMap (extractSpans' ss) members
109109 P.DataDeclaration _ name _ ctors ->
110110 (Right (runProperNameT name), ss)
src/Language/PureScript/Interactive/Completion.hs+1−1
@@ -206,7 +206,7 @@ identNames = nubOnFst . concatMap getDeclNames . P.exportedDeclarations
206206 getDeclNames d@(P.ValueDeclaration ident _ _ _) = [(ident, d)]
207207 getDeclNames d@(P.TypeDeclaration ident _ ) = [(ident, d)]
208208 getDeclNames d@(P.ExternDeclaration ident _) = [(ident, d)]
209− getDeclNames d@(P.TypeClassDeclaration _ _ _ ds) = map (second (const d)) $ concatMap getDeclNames ds
209+ getDeclNames d@(P.TypeClassDeclaration _ _ _ _ ds) = map (second (const d)) $ concatMap getDeclNames ds
210210 getDeclNames (P.PositionedDeclaration _ _ d) = getDeclNames d
211211 getDeclNames _ = []
212212
src/Language/PureScript/Interactive/Printer.hs+10−10
@@ -44,34 +44,34 @@ printModuleSignatures moduleName P.Environment{..} =
4444 showNameType _ = P.internalError "The impossible happened in printModuleSignatures."
4545
4646 findTypeClass
47− :: M.Map (P.Qualified (P.ProperName 'P.ClassName)) ([(String, Maybe P.Kind)], [(P.Ident, P.Type)], [P.Constraint])
47+ :: M.Map (P.Qualified (P.ProperName 'P.ClassName)) P.TypeClassData
4848 -> P.Qualified (P.ProperName 'P.ClassName)
49− -> (P.Qualified (P.ProperName 'P.ClassName), Maybe ([(String, Maybe P.Kind)], [(P.Ident, P.Type)], [P.Constraint]))
49+ -> (P.Qualified (P.ProperName 'P.ClassName), Maybe P.TypeClassData)
5050 findTypeClass envTypeClasses name = (name, M.lookup name envTypeClasses)
5151
5252 showTypeClass
53− :: (P.Qualified (P.ProperName 'P.ClassName), Maybe ([(String, Maybe P.Kind)], [(P.Ident, P.Type)], [P.Constraint]))
53+ :: (P.Qualified (P.ProperName 'P.ClassName), Maybe P.TypeClassData)
5454 -> Maybe Box.Box
5555 showTypeClass (_, Nothing) = Nothing
56− showTypeClass (P.Qualified _ name, Just (vars, body, constrs)) =
56+ showTypeClass (P.Qualified _ name, Just P.TypeClassData{..}) =
5757 let constraints =
58− if null constrs
58+ if null typeClassSuperclasses
5959 then Box.text ""
6060 else Box.text "("
61− Box.<> Box.hcat Box.left (intersperse (Box.text ", ") $ map (\(P.Constraint (P.Qualified _ pn) lt _) -> Box.text (P.runProperName pn) Box.<+> Box.hcat Box.left (map P.typeAtomAsBox lt)) constrs)
61+ Box.<> Box.hcat Box.left (intersperse (Box.text ", ") $ map (\(P.Constraint (P.Qualified _ pn) lt _) -> Box.text (P.runProperName pn) Box.<+> Box.hcat Box.left (map P.typeAtomAsBox lt)) typeClassSuperclasses)
6262 Box.<> Box.text ") <= "
6363 className =
6464 Box.text (P.runProperName name)
65− Box.<> Box.text (concatMap ((' ':) . fst) vars)
65+ Box.<> Box.text (concatMap ((' ':) . fst) typeClassArguments)
6666 classBody =
67− Box.vcat Box.top (map (\(i, t) -> Box.text (P.showIdent i ++ " ::") Box.<+> P.typeAsBox t) body)
67+ Box.vcat Box.top (map (\(i, t) -> Box.text (P.showIdent i ++ " ::") Box.<+> P.typeAsBox t) typeClassMembers)
6868
6969 in
7070 Just $
7171 (Box.text "class "
7272 Box.<> constraints
7373 Box.<> className
74− Box.<+> if null body then Box.text "" else Box.text "where")
74+ Box.<+> if null typeClassMembers then Box.text "" else Box.text "where")
7575 Box.// Box.moveRight 2 classBody
7676
7777
@@ -82,7 +82,7 @@ printModuleSignatures moduleName P.Environment{..} =
8282 findType envTypes name = (name, M.lookup name envTypes)
8383
8484 showType
85− :: M.Map (P.Qualified (P.ProperName 'P.ClassName)) ([(String, Maybe P.Kind)], [(P.Ident, P.Type)], [P.Constraint])
85+ :: M.Map (P.Qualified (P.ProperName 'P.ClassName)) P.TypeClassData
8686 -> M.Map (P.Qualified (P.ProperName 'P.ConstructorName)) (P.DataDeclType, P.ProperName 'P.TypeName, P.Type, [P.Ident])
8787 -> M.Map (P.Qualified (P.ProperName 'P.TypeName)) ([(String, Maybe P.Kind)], P.Type)
8888 -> (P.Qualified (P.ProperName 'P.TypeName), Maybe (P.Kind, P.TypeKind))
src/Language/PureScript/Parser/Declarations.hs+6−1
@@ -184,10 +184,15 @@ parseTypeClassDeclaration = do
184184 return implies
185185 className <- indented *> properName
186186 idents <- P.many (indented *> kindedIdent)
187+ let parseNamedIdent = foldl (<|>) empty (zipWith (\(name, _) index -> lname' name $> index) idents [0..])
188+ parseFunctionalDependency =
189+ FunctionalDependency <$> P.many parseNamedIdent <* rarrow
190+ <*> P.many parseNamedIdent
191+ dependencies <- P.option [] (indented *> pipe *> commaSep1 parseFunctionalDependency)
187192 members <- P.option [] $ do
188193 indented *> reserved "where"
189194 indented *> mark (P.many (same *> positioned parseTypeDeclaration))
190− return $ TypeClassDeclaration className idents implies members
195+ return $ TypeClassDeclaration className idents implies dependencies members
191196
192197parseConstraint :: TokenParser Constraint
193198parseConstraint = Constraint <$> parseQualified properName
src/Language/PureScript/Parser/Lexer.hs+7
@@ -40,6 +40,7 @@ module Language.PureScript.Parser.Lexer
4040 , commaSep
4141 , commaSep1
4242 , lname
43+ , lname'
4344 , qualifier
4445 , tyname
4546 , uname
@@ -414,6 +415,12 @@ lname = token go P.<?> "identifier"
414415 go (LName s) = Just s
415416 go _ = Nothing
416417
418+lname' :: String -> TokenParser ()
419+lname' s = token go P.<?> show s
420+ where
421+ go (LName s') | s == s' = Just ()
422+ go _ = Nothing
423+
417424qualifier :: TokenParser String
418425qualifier = token go P.<?> "qualifier"
419426 where
src/Language/PureScript/Pretty/Types.hs+1−1
@@ -45,7 +45,7 @@ typeLiterals = mkPattern match
4545 match _ = Nothing
4646
4747constraintsAsBox :: [Constraint] -> Box -> Box
48−constraintsAsBox [(Constraint pn tys _)] ty = text "(" <> constraintAsBox pn tys <> text ") => " <> ty
48+constraintsAsBox [(Constraint pn tys _)] ty = text "(" <> constraintAsBox pn tys `before` (text ") => " <> ty)
4949constraintsAsBox xs ty = vcat left (zipWith (\i (Constraint pn tys _) -> text (if i == 0 then "( " else ", ") <> constraintAsBox pn tys) [0 :: Int ..] xs) `before` (text ") => " <> ty)
5050
5151constraintAsBox :: Qualified (ProperName a) -> [Type] -> Box
src/Language/PureScript/Sugar/Names.hs+2−2
@@ -171,8 +171,8 @@ renameInModule imports (Module ss coms mn decls exps) =
171171 (,) (pos, bound) <$> (DataDeclaration dtype name args <$> traverse (sndM (traverse (updateTypesEverywhere pos))) dctors)
172172 updateDecl (pos, bound) (TypeSynonymDeclaration name ps ty) =
173173 (,) (pos, bound) <$> (TypeSynonymDeclaration name ps <$> updateTypesEverywhere pos ty)
174− updateDecl (pos, bound) (TypeClassDeclaration className args implies ds) =
175− (,) (pos, bound) <$> (TypeClassDeclaration className args <$> updateConstraints pos implies <*> pure ds)
174+ updateDecl (pos, bound) (TypeClassDeclaration className args implies deps ds) =
175+ (,) (pos, bound) <$> (TypeClassDeclaration className args <$> updateConstraints pos implies <*> pure deps <*> pure ds)
176176 updateDecl (pos, bound) (TypeInstanceDeclaration name cs cn ts ds) =
177177 (,) (pos, bound) <$> (TypeInstanceDeclaration name <$> updateConstraints pos cs <*> updateClassName cn pos <*> traverse (updateTypesEverywhere pos) ts <*> pure ds)
178178 updateDecl (pos, bound) (TypeDeclaration name ty) =
src/Language/PureScript/Sugar/Names/Exports.hs+1−1
@@ -30,7 +30,7 @@ findExportable (Module _ _ mn ds _) =
3030 rethrow (addHint (ErrorInModule mn)) $ foldM updateExports nullExports ds
3131 where
3232 updateExports :: Exports -> Declaration -> m Exports
33− updateExports exps (TypeClassDeclaration tcn _ _ ds') = do
33+ updateExports exps (TypeClassDeclaration tcn _ _ _ ds') = do
3434 exps' <- exportTypeClass Internal exps tcn mn
3535 foldM go exps' ds'
3636 where
src/Language/PureScript/Sugar/Operators.hs+2−2
@@ -312,9 +312,9 @@ updateTypes goType = (goDecl, goExpr, goBinder)
312312 goDecl pos (ExternDeclaration name ty) = do
313313 ty' <- goType' pos ty
314314 return (pos, ExternDeclaration name ty')
315− goDecl pos (TypeClassDeclaration name args implies decls) = do
315+ goDecl pos (TypeClassDeclaration name args implies deps decls) = do
316316 implies' <- traverse (overConstraintArgs (traverse (goType' pos))) implies
317− return (pos, TypeClassDeclaration name args implies' decls)
317+ return (pos, TypeClassDeclaration name args implies' deps decls)
318318 goDecl pos (TypeInstanceDeclaration name cs className tys impls) = do
319319 cs' <- traverse (overConstraintArgs (traverse (goType' pos))) cs
320320 tys' <- traverse (goType' pos) tys
src/Language/PureScript/Sugar/TypeClasses.hs+19−16
@@ -30,7 +30,7 @@ import Data.Maybe (catMaybes, mapMaybe, isJust)
3030
3131import qualified Data.Map as M
3232
33−type MemberMap = M.Map (ModuleName, ProperName 'ClassName) ([(String, Maybe Kind)], [Constraint], [Declaration])
33+type MemberMap = M.Map (ModuleName, ProperName 'ClassName) TypeClassData
3434
3535type Desugar = StateT MemberMap
3636
@@ -46,14 +46,20 @@ desugarTypeClasses
4646desugarTypeClasses externs = flip evalStateT initialState . traverse desugarModule
4747 where
4848 initialState :: MemberMap
49− initialState = M.singleton (ModuleName [ProperName C.prim], ProperName C.partial) ([], [], [])
50− `M.union` M.fromList (externs >>= \ExternsFile{..} -> mapMaybe (fromExternsDecl efModuleName) efDeclarations)
49+ initialState =
50+ M.mapKeys (qualify (ModuleName [ProperName C.prim])) primClasses
51+ `M.union` M.fromList (externs >>= \ExternsFile{..} -> mapMaybe (fromExternsDecl efModuleName) efDeclarations)
5152
5253 fromExternsDecl
5354 :: ModuleName
5455 -> ExternsDeclaration
55− -> Maybe ((ModuleName, ProperName 'ClassName), ([(String, Maybe Kind)], [Constraint], [Declaration]))
56− fromExternsDecl mn (EDClass name args members implies) = Just ((mn, name), (args, implies, map (uncurry TypeDeclaration) members))
56+ -> Maybe ((ModuleName, ProperName 'ClassName), TypeClassData)
57+ fromExternsDecl mn (EDClass name args members implies deps) = Just ((mn, name), typeClass) where
58+ typeClass = TypeClassData { typeClassArguments = args
59+ , typeClassMembers = members
60+ , typeClassSuperclasses = implies
61+ , typeClassDependencies = deps
62+ }
5763 fromExternsDecl _ _ = Nothing
5864
5965desugarModule
@@ -173,8 +179,8 @@ desugarDecl
173179 -> Desugar m (Maybe DeclarationRef, [Declaration])
174180desugarDecl mn exps = go
175181 where
176− go d@(TypeClassDeclaration name args implies members) = do
177− modify (M.insert (mn, name) (args, implies, members))
182+ go d@(TypeClassDeclaration name args implies deps members) = do
183+ modify (M.insert (mn, name) (TypeClassData args (map memberToNameAndType members) implies deps))
178184 return (Nothing, d : typeClassDictionaryDeclaration name args implies members : map (typeClassMemberToDictionaryAccessor mn name args) members)
179185 go (TypeInstanceDeclaration _ _ _ _ DerivedInstance) = internalError "Derived instanced should have been desugared"
180186 go d@(TypeInstanceDeclaration name deps className tys (ExplicitInstance members)) = do
@@ -271,18 +277,15 @@ typeInstanceDictionaryDeclaration name mn deps className tys decls =
271277 m <- get
272278
273279 -- Lookup the type arguments and member types for the type class
274− (args, implies, tyDecls) <-
280+ TypeClassData{..} <-
275281 maybe (throwError . errorMessage . UnknownName $ fmap TyClassName className) return $
276282 M.lookup (qualify mn className) m
277283
278− case mapMaybe declName tyDecls \\ mapMaybe declName decls of
284+ case map fst typeClassMembers \\ mapMaybe declName decls of
279285 member : _ -> throwError . errorMessage $ MissingClassMember member
280286 [] -> do
281−
282− let instanceTys = map memberToNameAndType tyDecls
283−
284287 -- Replace the type arguments with the appropriate types in the member types
285− let memberTypes = map (second (replaceAllTypeVars (zip (map fst args) tys))) instanceTys
288+ let memberTypes = map (second (replaceAllTypeVars (zip (map fst typeClassArguments) tys))) typeClassMembers
286289
287290 -- Create values for the type instance members
288291 members <- zip (map typeClassMemberName decls) <$> traverse (memberToValue memberTypes) decls
@@ -290,10 +293,10 @@ typeInstanceDictionaryDeclaration name mn deps className tys decls =
290293 -- Create the type of the dictionary
291294 -- The type is a record type, but depending on type instance dependencies, may be constrained.
292295 -- The dictionary itself is a record literal.
293− let superclasses = superClassDictionaryNames implies `zip`
296+ let superclasses = superClassDictionaryNames typeClassSuperclasses `zip`
294297 [ Abs (Left (Ident C.__unused)) (DeferredDictionary superclass tyArgs)
295− | (Constraint superclass suTyArgs _) <- implies
296− , let tyArgs = map (replaceAllTypeVars (zip (map fst args) tys)) suTyArgs
298+ | (Constraint superclass suTyArgs _) <- typeClassSuperclasses
299+ , let tyArgs = map (replaceAllTypeVars (zip (map fst typeClassArguments) tys)) suTyArgs
297300 ]
298301
299302 let props = Literal $ ObjectLiteral (members ++ superclasses)
src/Language/PureScript/TypeChecker.hs+17−9
@@ -112,15 +112,23 @@ addTypeClass
112112 -> ProperName 'ClassName
113113 -> [(String, Maybe Kind)]
114114 -> [Constraint]
115+ -> [FunctionalDependency]
115116 -> [Declaration]
116117 -> m ()
117−addTypeClass moduleName pn args implies ds =
118− let members = map toPair ds in
119− modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) (args, members, implies) (typeClasses . checkEnv $ st) } }
118+addTypeClass moduleName pn args implies dependencies ds =
119+ modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) newClass (typeClasses . checkEnv $ st) } }
120120 where
121− toPair (TypeDeclaration ident ty) = (ident, ty)
122− toPair (PositionedDeclaration _ _ d) = toPair d
123− toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
121+ newClass :: TypeClassData
122+ newClass =
123+ TypeClassData { typeClassArguments = args
124+ , typeClassMembers = map toPair ds
125+ , typeClassSuperclasses = implies
126+ , typeClassDependencies = dependencies
127+ }
128+
129+ toPair (TypeDeclaration ident ty) = (ident, ty)
130+ toPair (PositionedDeclaration _ _ d) = toPair d
131+ toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
124132
125133addTypeClassDictionaries
126134 :: (MonadState CheckState m)
@@ -265,8 +273,8 @@ typeCheckAll moduleName _ = traverse go
265273 return d
266274 go d@FixityDeclaration{} = return d
267275 go d@ImportDeclaration{} = return d
268− go d@(TypeClassDeclaration pn args implies tys) = do
269− addTypeClass moduleName pn args implies tys
276+ go d@(TypeClassDeclaration pn args implies deps tys) = do
277+ addTypeClass moduleName pn args implies deps tys
270278 return d
271279 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do
272280 traverse_ (checkTypeClassInstance moduleName) tys
@@ -414,7 +422,7 @@ typeCheckModule (Module ss coms mn decls (Just exps)) =
414422 unless (null missingMembers) $ throwError . errorMessage $ TransitiveExportError dr members
415423 where
416424 findClassMembers :: Declaration -> Maybe [Ident]
417− findClassMembers (TypeClassDeclaration name' _ _ ds) | name == name' = Just $ map extractMemberName ds
425+ findClassMembers (TypeClassDeclaration name' _ _ _ ds) | name == name' = Just $ map extractMemberName ds
418426 findClassMembers (PositionedDeclaration _ _ d) = findClassMembers d
419427 findClassMembers _ = Nothing
420428 extractMemberName :: Declaration -> Ident
src/Language/PureScript/TypeChecker/Entailment.hs+355−148
@@ -1,28 +1,35 @@
1+{-# LANGUAGE NamedFieldPuns #-}
2+
13-- |
24-- Type class entailment
35--
46module Language.PureScript.TypeChecker.Entailment
57 ( InstanceContext
68 , replaceTypeClassDictionaries
9+ , newDictionaries
710 ) where
811
912import Prelude.Compat
1013
14+import Control.Arrow (second)
1115import Control.Monad.Error.Class (MonadError(..))
1216import Control.Monad.State
1317import Control.Monad.Supply.Class (MonadSupply(..))
1418import Control.Monad.Writer
1519
20+import Data.Foldable (for_)
1621import Data.Function (on)
17−import Data.List (minimumBy, sortBy, groupBy)
18−import Data.Maybe (maybeToList, mapMaybe)
22+import Data.List (minimumBy, nub)
23+import Data.Maybe (fromMaybe, maybeToList, mapMaybe)
1924import qualified Data.Map as M
25+import qualified Data.Set as S
2026
2127import Language.PureScript.AST
2228import Language.PureScript.Crash
29+import Language.PureScript.Environment
2330import Language.PureScript.Errors
2431import Language.PureScript.Names
25−import Language.PureScript.TypeChecker.Monad (CheckState, withErrorMessageHint)
32+import Language.PureScript.TypeChecker.Monad
2633import Language.PureScript.TypeChecker.Unify
2734import Language.PureScript.TypeClassDictionaries
2835import Language.PureScript.Types
@@ -34,24 +41,57 @@ type InstanceContext = M.Map (Maybe ModuleName)
3441 (M.Map (Qualified Ident)
3542 TypeClassDictionaryInScope))
3643
37−-- | Merge two type class contexts
44+-- | A type substitution which makes an instance head match a list of types.
45+--
46+-- Note: we store many types per type variable name. For any name, all types
47+-- should unify if we are going to commit to an instance.
48+type Matching a = M.Map String a
49+
3850combineContexts :: InstanceContext -> InstanceContext -> InstanceContext
3951combineContexts = M.unionWith (M.unionWith M.union)
4052
4153-- | Replace type class dictionary placeholders with inferred type class dictionaries
4254replaceTypeClassDictionaries
43− :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
55+ :: forall m
56+ . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
4457 => Bool
45− -> ModuleName
4658 -> Expr
4759 -> m (Expr, [(Ident, Constraint)])
48−replaceTypeClassDictionaries shouldGeneralize mn =
49− let (_, f, _) = everywhereOnValuesTopDownM return (WriterT . go) return
50− in flip evalStateT M.empty . runWriterT . f
60+replaceTypeClassDictionaries shouldGeneralize expr = flip evalStateT M.empty $ do
61+ -- Loop, deferring any unsolved constraints, until there are no more
62+ -- constraints which can be solved, then make a generalization pass.
63+ let loop e = do
64+ (e', solved) <- deferPass e
65+ if getAny solved
66+ then loop e'
67+ else return e'
68+ loop expr >>= generalizePass
5169 where
52− go (TypeClassDictionary constraint dicts hints) =
53− rethrow (addHints hints) $ entails shouldGeneralize mn dicts constraint
54− go other = return (other, [])
70+ -- This pass solves constraints where possible, deferring constraints if not.
71+ deferPass :: Expr -> StateT InstanceContext m (Expr, Any)
72+ deferPass = fmap (second fst) . runWriterT . f where
73+ f :: Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
74+ (_, f, _) = everywhereOnValuesTopDownM return (go True) return
75+
76+ -- This pass generalizes any remaining constraints
77+ generalizePass :: Expr -> StateT InstanceContext m (Expr, [(Ident, Constraint)])
78+ generalizePass = fmap (second snd) . runWriterT . f where
79+ f :: Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
80+ (_, f, _) = everywhereOnValuesTopDownM return (go False) return
81+
82+ go :: Bool -> Expr -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
83+ go deferErrors dict@(TypeClassDictionary _ _ hints) =
84+ rethrow (addHints hints) $ entails shouldGeneralize deferErrors dict
85+ go _ other = return other
86+
87+-- | Three options for how we can handle a constraint, depending on the mode we're in.
88+data EntailsResult a
89+ = Solved a TypeClassDictionaryInScope
90+ -- ^ We solved this constraint
91+ | Unsolved Constraint
92+ -- ^ We couldn't solve this constraint right now, it will be generalized
93+ | Deferred
94+ -- ^ We couldn't solve this constraint right now, so it has been deferred
5595
5696-- |
5797-- Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
@@ -61,14 +101,14 @@ entails
61101 :: forall m
62102 . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
63103 => Bool
64− -> ModuleName
65− -> InstanceContext
66− -> Constraint
67− -> StateT InstanceContext m (Expr, [(Ident, Constraint)])
68−entails shouldGeneralize moduleName context = solve
104+ -> Bool
105+ -> Expr
106+ -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
107+entails shouldGeneralize deferErrors (TypeClassDictionary constraint context hints) =
108+ solve constraint
69109 where
70110 forClassName :: InstanceContext -> Qualified (ProperName 'ClassName) -> [Type] -> [TypeClassDictionaryInScope]
71− forClassName ctx cn@(Qualified (Just mn) _) tys = concatMap (findDicts ctx cn) (Nothing : Just mn : map Just (mapMaybe ctorModules tys))
111+ forClassName ctx cn@(Qualified (Just mn) _) tys = concatMap (findDicts ctx cn) (nub (Nothing : Just mn : map Just (mapMaybe ctorModules tys)))
72112 forClassName _ _ _ = internalError "forClassName: expected qualified class name"
73113
74114 ctorModules :: Type -> Maybe ModuleName
@@ -80,139 +120,306 @@ entails shouldGeneralize moduleName context = solve
80120 findDicts :: InstanceContext -> Qualified (ProperName 'ClassName) -> Maybe ModuleName -> [TypeClassDictionaryInScope]
81121 findDicts ctx cn = maybe [] M.elems . (>>= M.lookup cn) . flip M.lookup ctx
82122
83− solve :: Constraint -> StateT InstanceContext m (Expr, [(Ident, Constraint)])
84− solve con = StateT . (withErrorMessageHint (ErrorSolvingConstraint con) .) . runStateT $ do
85− (dict, unsolved) <- go 0 con
86− return (dictionaryValueToValue dict, unsolved)
123+ valUndefined :: Expr
124+ valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
125+
126+ solve :: Constraint -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
127+ solve con = go 0 con
87128 where
88− go :: Int -> Constraint -> StateT InstanceContext m (DictionaryValue, [(Ident, Constraint)])
89− go work (Constraint className' tys' _) | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
90− go work con'@(Constraint className' tys' _) = do
91− -- Get the inferred constraint context so far, and merge it with the global context
92− inferred <- get
93− let instances = do
94− tcd <- forClassName (combineContexts context inferred) className' tys'
95− -- Make sure the type unifies with the type in the type instance definition
96− subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName) tys' (tcdInstanceTypes tcd)
97− return (subst, tcd)
98− solution <- lift $ unique instances
99− case solution of
100− Left (subst, tcd) -> do
101− -- Solve any necessary subgoals
102− (args, unsolved) <- solveSubgoals subst (tcdDependencies tcd)
103− let match = foldr (\(superclassName, index) dict -> SubclassDictionaryValue dict superclassName index)
104− (mkDictionary (tcdName tcd) args)
105− (tcdPath tcd)
106− return (match, unsolved)
107− Right unsolved@(Constraint unsolvedClassName@(Qualified _ pn) unsolvedTys _) -> do
108− -- Generate a fresh name for the unsolved constraint's new dictionary
109− ident <- freshIdent ("dict" ++ runProperName pn)
110− let qident = Qualified Nothing ident
111− -- Store the new dictionary in the InstanceContext so that we can solve this goal in
112− -- future.
113− let newDict = TypeClassDictionaryInScope qident [] unsolvedClassName unsolvedTys Nothing
114− newContext = M.singleton Nothing (M.singleton unsolvedClassName (M.singleton qident newDict))
115− modify (combineContexts newContext)
116− return (LocalDictionaryValue qident, [(ident, unsolved)])
117− where
129+ go :: Int -> Constraint -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) Expr
130+ go work (Constraint className' tys' _) | work > 1000 = throwError . errorMessage $ PossiblyInfiniteInstance className' tys'
131+ go work con'@(Constraint className' tys' conInfo) = WriterT . StateT . (withErrorMessageHint (ErrorSolvingConstraint con') .) . runStateT . runWriterT $ do
132+ -- We might have unified types by solving other constraints, so we need to
133+ -- apply the latest substitution.
134+ latestSubst <- lift . lift $ gets checkSubstitution
135+ let tys'' = map (substituteType latestSubst) tys'
136+ -- Get the inferred constraint context so far, and merge it with the global context
137+ inferred <- lift get
138+ -- We need information about functional dependencies, so we have to look up the class
139+ -- name in the environment:
140+ let findClass = fromMaybe (internalError "entails: type class not found in environment") . M.lookup className'
141+ TypeClassData{ typeClassDependencies } <- lift . lift $ gets (findClass . typeClasses . checkEnv)
142+ let instances =
143+ [ (substs, tcd)
144+ | tcd <- forClassName (combineContexts context inferred) className' tys''
145+ -- Make sure the type unifies with the type in the type instance definition
146+ , substs <- maybeToList (matches typeClassDependencies tcd tys'')
147+ ]
148+ solution <- lift . lift $ unique tys'' instances
149+ case solution of
150+ Solved substs tcd -> do
151+ -- Note that we solved something.
152+ tell (Any True, mempty)
153+ -- Make sure the substitution is valid:
154+ lift . lift . for_ substs $ pairwiseM unifyTypes
155+ -- Now enforce any functional dependencies, using unification
156+ -- Note: we need to generate fresh types for any unconstrained
157+ -- type variables before unifying.
158+ let subst = fmap head substs
159+ currentSubst <- lift . lift $ gets checkSubstitution
160+ subst' <- lift . lift $ withFreshTypes tcd (fmap (substituteType currentSubst) subst)
161+ lift . lift $ zipWithM_ (\t1 t2 -> do
162+ let inferredType = replaceAllTypeVars (M.toList subst') t1
163+ unifyTypes inferredType t2) (tcdInstanceTypes tcd) tys''
164+ currentSubst' <- lift . lift $ gets checkSubstitution
165+ let subst'' = fmap (substituteType currentSubst') subst'
166+ -- Solve any necessary subgoals
167+ args <- solveSubgoals subst'' (tcdDependencies tcd)
168+ let match = foldr (\(superclassName, index) dict -> subclassDictionaryValue dict superclassName index)
169+ (mkDictionary (tcdName tcd) args)
170+ (tcdPath tcd)
171+ return match
172+ Unsolved unsolved -> do
173+ -- Generate a fresh name for the unsolved constraint's new dictionary
174+ ident <- freshIdent ("dict" ++ runProperName (disqualify (constraintClass unsolved)))
175+ let qident = Qualified Nothing ident
176+ -- Store the new dictionary in the InstanceContext so that we can solve this goal in
177+ -- future.
178+ newDicts <- lift . lift $ newDictionaries [] qident unsolved
179+ let newContext = mkContext newDicts
180+ modify (combineContexts newContext)
181+ -- Mark this constraint for generalization
182+ tell (mempty, [(ident, unsolved)])
183+ return (Var qident)
184+ Deferred ->
185+ -- Constraint was deferred, just return the dictionary unchanged,
186+ -- with no unsolved constraints. Hopefully, we can solve this later.
187+ return (TypeClassDictionary (Constraint className' tys'' conInfo) context hints)
188+ where
189+ -- | When checking functional dependencies, we need to use unification to make
190+ -- sure it is safe to use the selected instance. We will unify the solved type with
191+ -- the type in the instance head under the substition inferred from its instantiation.
192+ -- As an example, when solving MonadState t0 (State Int), we choose the
193+ -- MonadState s (State s) instance, and we unify t0 with Int, since the functional
194+ -- dependency from MonadState dictates that t0 should unify with s\[s -> Int], which is
195+ -- Int. This is fine, but in some cases, the substitution does not remove all TypeVars
196+ -- from the type, so we end up with a unification error. So, any type arguments which
197+ -- appear in the instance head, but not in the substitution need to be replaced with
198+ -- fresh type variables. This function extends a substitution with fresh type variables
199+ -- as necessary, based on the types in the instance head.
200+ withFreshTypes
201+ :: TypeClassDictionaryInScope
202+ -> Matching Type
203+ -> m (Matching Type)
204+ withFreshTypes TypeClassDictionaryInScope{..} subst = do
205+ let onType = everythingOnTypes S.union fromTypeVar
206+ typeVarsInHead = foldMap onType tcdInstanceTypes
207+ <> foldMap (foldMap (foldMap onType . constraintArgs)) tcdDependencies
208+ typeVarsInSubst = S.fromList (M.keys subst)
209+ uninstantiatedTypeVars = typeVarsInHead S.\\ typeVarsInSubst
210+ newSubst <- traverse withFreshType (S.toList uninstantiatedTypeVars)
211+ return (subst <> M.fromList newSubst)
212+ where
213+ fromTypeVar (TypeVar v) = S.singleton v
214+ fromTypeVar _ = S.empty
118215
119− unique :: [(a, TypeClassDictionaryInScope)] -> m (Either (a, TypeClassDictionaryInScope) Constraint)
120− unique [] | shouldGeneralize && all canBeGeneralized tys' = return (Right con')
121− | otherwise = throwError . errorMessage $ NoInstanceFound con'
122− unique [a] = return $ Left a
123− unique tcds | pairwise overlapping (map snd tcds) = do
124− tell . errorMessage $ OverlappingInstances className' tys' (map (tcdName . snd) tcds)
125− return $ Left (head tcds)
126− | otherwise = return $ Left (minimumBy (compare `on` length . tcdPath . snd) tcds)
127−
128− canBeGeneralized :: Type -> Bool
129− canBeGeneralized TUnknown{} = True
130− canBeGeneralized Skolem{} = True
131− canBeGeneralized _ = False
132−
133− -- |
134− -- Check if two dictionaries are overlapping
135− --
136− -- Dictionaries which are subclass dictionaries cannot overlap, since otherwise the overlap would have
137− -- been caught when constructing superclass dictionaries.
138− overlapping :: TypeClassDictionaryInScope -> TypeClassDictionaryInScope -> Bool
139− overlapping TypeClassDictionaryInScope{ tcdPath = _ : _ } _ = False
140− overlapping _ TypeClassDictionaryInScope{ tcdPath = _ : _ } = False
141− overlapping TypeClassDictionaryInScope{ tcdDependencies = Nothing } _ = False
142− overlapping _ TypeClassDictionaryInScope{ tcdDependencies = Nothing } = False
143− overlapping tcd1 tcd2 = tcdName tcd1 /= tcdName tcd2
144−
145− -- Create dictionaries for subgoals which still need to be solved by calling go recursively
146− -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
147− -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
148− solveSubgoals :: [(String, Type)] -> Maybe [Constraint] -> StateT InstanceContext m (Maybe [DictionaryValue], [(Ident, Constraint)])
149− solveSubgoals _ Nothing = return (Nothing, [])
150− solveSubgoals subst (Just subgoals) = do
151− zipped <- traverse (go (work + 1) . mapConstraintArgs (map (replaceAllTypeVars subst))) subgoals
152− let (dicts, unsolved) = unzip zipped
153− return (Just dicts, concat unsolved)
154−
155− -- Make a dictionary from subgoal dictionaries by applying the correct function
156− mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
157− mkDictionary fnName Nothing = LocalDictionaryValue fnName
158− mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
159− mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
160−
161− -- Turn a DictionaryValue into a Expr
162− dictionaryValueToValue :: DictionaryValue -> Expr
163− dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName
164− dictionaryValueToValue (GlobalDictionaryValue fnName) = Var fnName
165− dictionaryValueToValue (DependentDictionaryValue fnName dicts) = foldl App (Var fnName) (map dictionaryValueToValue dicts)
166− dictionaryValueToValue (SubclassDictionaryValue dict superclassName index) =
167− App (Accessor (C.__superclass_ ++ showQualified runProperName superclassName ++ "_" ++ show index)
168− (dictionaryValueToValue dict))
169− valUndefined
170− -- Ensure that a substitution is valid
171− verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
172− verifySubstitution subst = do
173− let grps = groupBy ((==) `on` fst) . sortBy (compare `on` fst) $ subst
174− guard (all (pairwise unifiesWith . map snd) grps)
175− return $ map head grps
216+ withFreshType s = do
217+ t <- freshType
218+ return (s, t)
176219
177− valUndefined :: Expr
178− valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
220+ unique :: [Type] -> [(a, TypeClassDictionaryInScope)] -> m (EntailsResult a)
221+ unique tyArgs []
222+ | deferErrors = return Deferred
223+ -- We need a special case for nullary type classes, since we want
224+ -- to generalize over Partial constraints.
225+ | shouldGeneralize && (null tyArgs || any canBeGeneralized tyArgs) = return (Unsolved (Constraint className' tyArgs conInfo))
226+ | otherwise = throwError . errorMessage $ NoInstanceFound (Constraint className' tyArgs conInfo)
227+ unique _ [(a, dict)] = return $ Solved a dict
228+ unique tyArgs tcds
229+ | pairwiseAny overlapping (map snd tcds) = do
230+ tell . errorMessage $ OverlappingInstances className' tyArgs (map (tcdName . snd) tcds)
231+ return $ uncurry Solved (head tcds)
232+ | otherwise = return $ uncurry Solved (minimumBy (compare `on` length . tcdPath . snd) tcds)
179233
180−-- |
181−-- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
182−-- and return a substitution from type variables to types which makes the type heads unify.
183−--
184−typeHeadsAreEqual :: ModuleName -> Type -> Type -> Maybe [(String, Type)]
185−typeHeadsAreEqual _ (TUnknown u1) (TUnknown u2) | u1 == u2 = Just []
186−typeHeadsAreEqual _ (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = Just []
187−typeHeadsAreEqual _ t (TypeVar v) = Just [(v, t)]
188−typeHeadsAreEqual _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
189−typeHeadsAreEqual _ (TypeLevelString s1) (TypeLevelString s2) | s1 == s2 = Just []
190−typeHeadsAreEqual m (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m h1 h2
191− <*> typeHeadsAreEqual m t1 t2
192−typeHeadsAreEqual _ REmpty REmpty = Just []
193−typeHeadsAreEqual m r1@RCons{} r2@RCons{} =
194− let (s1, r1') = rowToList r1
195− (s2, r2') = rowToList r2
196−
197− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
198− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
199− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
200− in (++) <$> foldMap (uncurry (typeHeadsAreEqual m)) int
201− <*> go sd1 r1' sd2 r2'
234+ canBeGeneralized :: Type -> Bool
235+ canBeGeneralized TUnknown{} = True
236+ canBeGeneralized Skolem{} = True
237+ canBeGeneralized _ = False
238+
239+ -- |
240+ -- Check if two dictionaries are overlapping
241+ --
242+ -- Dictionaries which are subclass dictionaries cannot overlap, since otherwise the overlap would have
243+ -- been caught when constructing superclass dictionaries.
244+ overlapping :: TypeClassDictionaryInScope -> TypeClassDictionaryInScope -> Bool
245+ overlapping TypeClassDictionaryInScope{ tcdPath = _ : _ } _ = False
246+ overlapping _ TypeClassDictionaryInScope{ tcdPath = _ : _ } = False
247+ overlapping TypeClassDictionaryInScope{ tcdDependencies = Nothing } _ = False
248+ overlapping _ TypeClassDictionaryInScope{ tcdDependencies = Nothing } = False
249+ overlapping tcd1 tcd2 = tcdName tcd1 /= tcdName tcd2
250+
251+ -- Create dictionaries for subgoals which still need to be solved by calling go recursively
252+ -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
253+ -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
254+ solveSubgoals :: Matching Type -> Maybe [Constraint] -> WriterT (Any, [(Ident, Constraint)]) (StateT InstanceContext m) (Maybe [Expr])
255+ solveSubgoals _ Nothing = return Nothing
256+ solveSubgoals subst (Just subgoals) =
257+ Just <$> traverse (go (work + 1) . mapConstraintArgs (map (replaceAllTypeVars (M.toList subst)))) subgoals
258+
259+ -- Make a dictionary from subgoal dictionaries by applying the correct function
260+ mkDictionary :: Qualified Ident -> Maybe [Expr] -> Expr
261+ mkDictionary fnName Nothing = Var fnName
262+ mkDictionary fnName (Just []) = Var fnName
263+ mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
264+
265+ -- Turn a DictionaryValue into a Expr
266+ subclassDictionaryValue :: Expr -> Qualified (ProperName a) -> Integer -> Expr
267+ subclassDictionaryValue dict superclassName index =
268+ App (Accessor (C.__superclass_ ++ showQualified runProperName superclassName ++ "_" ++ show index)
269+ dict)
270+ valUndefined
271+entails _ _ _ = internalError "entails: expected TypeClassDictionary"
272+
273+-- Check if an instance matches our list of types, allowing for types
274+-- to be solved via functional dependencies. If the types match, we return a
275+-- substitution which makes them match. If not, we return 'Nothing'.
276+matches :: [FunctionalDependency] -> TypeClassDictionaryInScope -> [Type] -> Maybe (Matching [Type])
277+matches deps TypeClassDictionaryInScope{..} tys = do
278+ -- First, find those types which match exactly
279+ let matched = zipWith typeHeadsAreEqual tys tcdInstanceTypes
280+ -- Now, use any functional dependencies to infer any remaining types
281+ guard $ covers matched
282+ -- Verify that any repeated type variables are unifiable
283+ let determinedSet = foldMap (S.fromList . fdDetermined) deps
284+ solved = map snd . filter ((`S.notMember` determinedSet) . fst) $ zipWith (\(_, ts) i -> (i, ts)) matched [0..]
285+ verifySubstitution (M.unionsWith (++) solved)
202286 where
203− go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
204− go [] REmpty [] REmpty = Just []
205− go [] (TUnknown _) _ _ = Just []
206− go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = Just []
207− go [] (Skolem _ s1 _ _) [] (Skolem _ s2 _ _) | s1 == s2 = Just []
208− go sd r [] (TypeVar v) = Just [(v, rowFromList (sd, r))]
209− go _ _ _ _ = Nothing
210−typeHeadsAreEqual _ _ _ = Nothing
287+ -- | Find the closure of a set of functional dependencies.
288+ covers :: [(Bool, subst)] -> Bool
289+ covers ms = finalSet == S.fromList [0..length ms - 1]
290+ where
291+ initialSet :: S.Set Int
292+ initialSet = S.fromList . map snd . filter (fst . fst) $ zip ms [0..]
211293
212−-- |
213−-- Check all values in a list pairwise match a predicate
214−--
215−pairwise :: (a -> a -> Bool) -> [a] -> Bool
216−pairwise _ [] = True
217−pairwise _ [_] = True
218−pairwise p (x : xs) = all (p x) xs && pairwise p xs
294+ finalSet :: S.Set Int
295+ finalSet = untilFixedPoint applyAll initialSet
296+
297+ untilFixedPoint :: Eq a => (a -> a) -> a -> a
298+ untilFixedPoint f = go
299+ where
300+ go a | a' == a = a'
301+ | otherwise = go a'
302+ where a' = f a
303+
304+ applyAll :: S.Set Int -> S.Set Int
305+ applyAll s = foldr applyDependency s deps
306+
307+ applyDependency :: FunctionalDependency -> S.Set Int -> S.Set Int
308+ applyDependency FunctionalDependency{..} xs
309+ | S.fromList fdDeterminers `S.isSubsetOf` xs = xs <> S.fromList fdDetermined
310+ | otherwise = xs
311+
312+ --
313+ -- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
314+ -- and return a substitution from type variables to types which makes the type heads unify.
315+ --
316+ typeHeadsAreEqual :: Type -> Type -> (Bool, Matching [Type])
317+ typeHeadsAreEqual (TUnknown u1) (TUnknown u2) | u1 == u2 = (True, M.empty)
318+ typeHeadsAreEqual (Skolem _ s1 _ _) (Skolem _ s2 _ _) | s1 == s2 = (True, M.empty)
319+ typeHeadsAreEqual t (TypeVar v) = (True, M.singleton v [t])
320+ typeHeadsAreEqual (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = (True, M.empty)
321+ typeHeadsAreEqual (TypeLevelString s1) (TypeLevelString s2) | s1 == s2 = (True, M.empty)
322+ typeHeadsAreEqual (TypeApp h1 t1) (TypeApp h2 t2) =
323+ both (typeHeadsAreEqual h1 h2) (typeHeadsAreEqual t1 t2)
324+ typeHeadsAreEqual REmpty REmpty = (True, M.empty)
325+ typeHeadsAreEqual r1@RCons{} r2@RCons{} =
326+ foldr both (go sd1 r1' sd2 r2') (map (uncurry typeHeadsAreEqual) int)
327+ where
328+ (s1, r1') = rowToList r1
329+ (s2, r2') = rowToList r2
330+
331+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
332+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
333+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
334+
335+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> (Bool, Matching [Type])
336+ go [] REmpty [] REmpty = (True, M.empty)
337+ go [] (TUnknown u1) [] (TUnknown u2) | u1 == u2 = (True, M.empty)
338+ go [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = (True, M.empty)
339+ go [] (Skolem _ sk1 _ _) [] (Skolem _ sk2 _ _) | sk1 == sk2 = (True, M.empty)
340+ go sd r [] (TypeVar v) = (True, M.singleton v [rowFromList (sd, r)])
341+ go _ _ _ _ = (False, M.empty)
342+ typeHeadsAreEqual _ _ = (False, M.empty)
343+
344+ both :: (Bool, Matching [Type]) -> (Bool, Matching [Type]) -> (Bool, Matching [Type])
345+ both (b1, m1) (b2, m2) = (b1 && b2, M.unionWith (++) m1 m2)
346+
347+ -- Ensure that a substitution is valid
348+ verifySubstitution :: Matching [Type] -> Maybe (Matching [Type])
349+ verifySubstitution = traverse meet where
350+ meet ts | pairwiseAll typesAreEqual ts = Just ts
351+ | otherwise = Nothing
352+
353+ -- Note that unknowns are only allowed to unify if they came from a type
354+ -- which was _not_ solved, i.e. one which was inferred by a functional
355+ -- dependency.
356+ typesAreEqual :: Type -> Type -> Bool
357+ typesAreEqual (TUnknown u1) (TUnknown u2) | u1 == u2 = True
358+ typesAreEqual (Skolem _ s1 _ _) (Skolem _ s2 _ _) = s1 == s2
359+ typesAreEqual (TypeVar v1) (TypeVar v2) = v1 == v2
360+ typesAreEqual (TypeLevelString s1) (TypeLevelString s2) = s1 == s2
361+ typesAreEqual (TypeConstructor c1) (TypeConstructor c2) = c1 == c2
362+ typesAreEqual (TypeApp h1 t1) (TypeApp h2 t2) = typesAreEqual h1 h2 && typesAreEqual t1 t2
363+ typesAreEqual REmpty REmpty = True
364+ typesAreEqual r1 r2 | isRCons r1 || isRCons r2 =
365+ let (s1, r1') = rowToList r1
366+ (s2, r2') = rowToList r2
367+
368+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
369+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
370+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
371+ in all (uncurry typesAreEqual) int && go sd1 r1' sd2 r2'
372+ where
373+ go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
374+ go [] (TUnknown u1) [] (TUnknown u2) | u1 == u2 = True
375+ go [] (Skolem _ s1 _ _) [] (Skolem _ s2 _ _) = s1 == s2
376+ go [] REmpty [] REmpty = True
377+ go [] (TypeVar v1) [] (TypeVar v2) = v1 == v2
378+ go _ _ _ _ = False
379+ typesAreEqual _ _ = False
380+
381+ isRCons :: Type -> Bool
382+ isRCons RCons{} = True
383+ isRCons _ = False
384+
385+-- | Add a dictionary for the constraint to the scope, and dictionaries
386+-- for all implied superclass instances.
387+newDictionaries
388+ :: MonadState CheckState m
389+ => [(Qualified (ProperName 'ClassName), Integer)]
390+ -> Qualified Ident
391+ -> Constraint
392+ -> m [TypeClassDictionaryInScope]
393+newDictionaries path name (Constraint className instanceTy _) = do
394+ tcs <- gets (typeClasses . checkEnv)
395+ let TypeClassData{..} = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs
396+ supDicts <- join <$> zipWithM (\(Constraint supName supArgs _) index ->
397+ newDictionaries ((supName, index) : path)
398+ name
399+ (Constraint supName (instantiateSuperclass (map fst typeClassArguments) supArgs instanceTy) Nothing)
400+ ) typeClassSuperclasses [0..]
401+ return (TypeClassDictionaryInScope name path className instanceTy Nothing : supDicts)
402+ where
403+ instantiateSuperclass :: [String] -> [Type] -> [Type] -> [Type]
404+ instantiateSuperclass args supArgs tys = map (replaceAllTypeVars (zip args tys)) supArgs
405+
406+mkContext :: [TypeClassDictionaryInScope] -> InstanceContext
407+mkContext = foldr combineContexts M.empty . map fromDict where
408+ fromDict d = M.singleton Nothing (M.singleton (tcdClassName d) (M.singleton (tcdName d) d))
409+
410+-- | Check all pairs of values in a list match a predicate
411+pairwiseAll :: (a -> a -> Bool) -> [a] -> Bool
412+pairwiseAll _ [] = True
413+pairwiseAll _ [_] = True
414+pairwiseAll p (x : xs) = all (p x) xs && pairwiseAll p xs
415+
416+-- | Check any pair of values in a list match a predicate
417+pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
418+pairwiseAny _ [] = False
419+pairwiseAny _ [_] = False
420+pairwiseAny p (x : xs) = any (p x) xs || pairwiseAny p xs
421+
422+pairwiseM :: Applicative m => (a -> a -> m ()) -> [a] -> m ()
423+pairwiseM _ [] = pure ()
424+pairwiseM _ [_] = pure ()
425+pairwiseM p (x : xs) = traverse (p x) xs *> pairwiseM p xs
src/Language/PureScript/TypeChecker/Kinds.hs+7−8
@@ -16,7 +16,6 @@ import Control.Arrow (second)
1616import Control.Monad
1717import Control.Monad.Error.Class (MonadError(..))
1818import Control.Monad.State
19−import Control.Monad.Writer.Class (MonadWriter(..))
2019
2120import qualified Data.Map as M
2221
@@ -96,19 +95,19 @@ unifyKinds k1 k2 = do
9695
9796-- | Infer the kind of a single type
9897kindOf
99− :: (MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m)
98+ :: (MonadError MultipleErrors m, MonadState CheckState m)
10099 => Type
101100 -> m Kind
102101kindOf ty = fst <$> kindOfWithScopedVars ty
103102
104103-- | Infer the kind of a single type, returning the kinds of any scoped type variables
105104kindOfWithScopedVars ::
106− (MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m) =>
105+ (MonadError MultipleErrors m, MonadState CheckState m) =>
107106 Type ->
108107 m (Kind, [(String, Kind)])
109108kindOfWithScopedVars ty =
110109 withErrorMessageHint (ErrorCheckingKind ty) $
111− fmap tidyUp . liftUnify $ infer ty
110+ fmap tidyUp . withFreshSubstitution . captureSubstitution $ infer ty
112111 where
113112 tidyUp ((k, args), sub) = ( starIfUnknown (substituteKind sub k)
114113 , map (second (starIfUnknown . substituteKind sub)) args
@@ -116,14 +115,14 @@ kindOfWithScopedVars ty =
116115
117116-- | Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
118117kindsOf
119− :: (MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m)
118+ :: (MonadError MultipleErrors m, MonadState CheckState m)
120119 => Bool
121120 -> ModuleName
122121 -> ProperName 'TypeName
123122 -> [(String, Maybe Kind)]
124123 -> [Type]
125124 -> m Kind
126−kindsOf isData moduleName name args ts = fmap tidyUp . liftUnify $ do
125+kindsOf isData moduleName name args ts = fmap tidyUp . withFreshSubstitution . captureSubstitution $ do
127126 tyCon <- freshKind
128127 kargs <- replicateM (length args) freshKind
129128 rest <- zipWithM freshKindVar args kargs
@@ -145,12 +144,12 @@ freshKindVar (arg, Just kind') kind = do
145144
146145-- | Simultaneously infer the kinds of several mutually recursive type constructors
147146kindsOfAll
148− :: (MonadError MultipleErrors m, MonadState CheckState m, MonadWriter MultipleErrors m)
147+ :: (MonadError MultipleErrors m, MonadState CheckState m)
149148 => ModuleName
150149 -> [(ProperName 'TypeName, [(String, Maybe Kind)], Type)]
151150 -> [(ProperName 'TypeName, [(String, Maybe Kind)], [Type])]
152151 -> m ([Kind], [Kind])
153−kindsOfAll moduleName syns tys = fmap tidyUp . liftUnify $ do
152+kindsOfAll moduleName syns tys = fmap tidyUp . withFreshSubstitution . captureSubstitution $ do
154153 synVars <- replicateM (length syns) freshKind
155154 let dict = zipWith (\(name, _, _) var -> (name, var)) syns synVars
156155 bindLocalTypeVariables moduleName dict $ do
src/Language/PureScript/TypeChecker/Monad.hs+30−18
@@ -11,7 +11,7 @@ import Prelude.Compat
1111import Control.Arrow (second)
1212import Control.Monad.Error.Class (MonadError(..))
1313import Control.Monad.State
14−import Control.Monad.Writer.Class (MonadWriter(..), listen, censor)
14+import Control.Monad.Writer.Class (MonadWriter(..), censor)
1515
1616import Data.Maybe
1717import qualified Data.Map as M
@@ -269,23 +269,35 @@ guardWith _ True = return ()
269269guardWith e False = throwError e
270270
271271-- | Run a computation in the substitution monad, generating a return value and the final substitution.
272−liftUnify ::
273− (MonadState CheckState m, MonadWriter MultipleErrors m, MonadError MultipleErrors m) =>
274− m a ->
275− m (a, Substitution)
276−liftUnify = liftUnifyWarnings (const id)
277−
278−-- | Run a computation in the substitution monad, generating a return value, the final substitution and updating warnings values.
279−liftUnifyWarnings ::
280− (MonadState CheckState m, MonadWriter MultipleErrors m, MonadError MultipleErrors m) =>
281− (Substitution -> ErrorMessage -> ErrorMessage) ->
282− m a ->
283− m (a, Substitution)
284−liftUnifyWarnings replace ma = do
272+captureSubstitution
273+ :: MonadState CheckState m
274+ => m a
275+ -> m (a, Substitution)
276+captureSubstitution = capturingSubstitution (,)
277+
278+capturingSubstitution
279+ :: MonadState CheckState m
280+ => (a -> Substitution -> b)
281+ -> m a
282+ -> m b
283+capturingSubstitution f ma = do
284+ a <- ma
285+ subst <- gets checkSubstitution
286+ return (f a subst)
287+
288+withFreshSubstitution
289+ :: MonadState CheckState m
290+ => m a
291+ -> m a
292+withFreshSubstitution ma = do
285293 orig <- get
286294 modify $ \st -> st { checkSubstitution = emptySubstitution }
287− (a, w) <- reflectErrors . censor (const mempty) . reifyErrors . listen $ ma
288− subst <- gets checkSubstitution
289− tell . onErrorMessages (replace subst) $ w
295+ a <- ma
290296 modify $ \st -> st { checkSubstitution = checkSubstitution orig }
291− return (a, subst)
297+ return a
298+
299+withoutWarnings
300+ :: MonadWriter w m
301+ => m a
302+ -> m (a, w)
303+withoutWarnings = censor (const mempty) . listen
src/Language/PureScript/TypeChecker/Types.hs+69−75
@@ -1,4 +1,5 @@
11{-# LANGUAGE OverloadedStrings #-}
2+{-# LANGUAGE NamedFieldPuns #-}
23
34-- |
45-- This module implements the type checker
@@ -36,6 +37,7 @@ import Data.Either (lefts, rights)
3637import Data.List (transpose, nub, (\\), partition, delete)
3738import Data.Maybe (fromMaybe)
3839import qualified Data.Map as M
40+import qualified Data.Set as S
3941
4042import Language.PureScript.AST
4143import Language.PureScript.Crash
@@ -52,7 +54,6 @@ import Language.PureScript.TypeChecker.Skolems
5254import Language.PureScript.TypeChecker.Subsumption
5355import Language.PureScript.TypeChecker.Synonyms
5456import Language.PureScript.TypeChecker.Unify
55−import Language.PureScript.TypeClassDictionaries
5657import Language.PureScript.Types
5758
5859data BindingGroupType
@@ -62,65 +63,78 @@ data BindingGroupType
6263
6364-- | Infer the types of multiple mutually-recursive values, and return elaborated values including
6465-- type class dictionaries and type annotations.
65−typesOf ::
66− (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) =>
67− BindingGroupType ->
68− ModuleName ->
69− [(Ident, Expr)] ->
70− m [(Ident, (Expr, Type))]
71−typesOf bindingGroupType moduleName vals = do
72− tys <- fmap tidyUp . escalateWarningWhen isHoleError . liftUnifyWarnings replace $ do
73− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
74− ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
75− ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
76− return (map (\x -> (False, x)) ds1 ++ map (\x -> (True, x)) ds2)
77−
78− forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do
79− -- Replace type class dictionary placeholders with actual dictionaries
80− (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize moduleName val
81− let unsolvedTypeVars = nub $ unknownsInType ty
82− -- Generalize and constrain the type
83− let generalized = generalize unsolved ty
84−
85− when shouldGeneralize $ do
86− -- Show the inferred type in a warning
87− tell . errorMessage $ MissingTypeDeclaration ident generalized
88− -- For non-recursive binding groups, can generalize over constraints.
89− -- For recursive binding groups, we throw an error here for now.
90− when (bindingGroupType == RecursiveBindingGroup && not (null unsolved))
91− . throwError
92− . errorMessage
93− $ CannotGeneralizeRecursiveFunction ident generalized
94− -- Make sure any unsolved type constraints only use type variables which appear
95− -- unknown in the inferred type.
96− forM_ unsolved $ \(_, con) -> do
97− let constraintTypeVars = nub $ foldMap unknownsInType (constraintArgs con)
98− when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $
99− throwError . errorMessage $ NoInstanceFound con
100−
101− -- Check skolem variables did not escape their scope
102− skolemEscapeCheck val'
103− -- Check rows do not contain duplicate labels
104− checkDuplicateLabels val'
105− return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))
66+typesOf
67+ :: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
68+ => BindingGroupType
69+ -> ModuleName
70+ -> [(Ident, Expr)]
71+ -> m [(Ident, (Expr, Type))]
72+typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
73+ (tys, w) <- withoutWarnings . capturingSubstitution tidyUp $ do
74+ (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup (Just moduleName) vals
75+ ds1 <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
76+ ds2 <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
77+ return (map (\x -> (False, x)) ds1 ++ map (\x -> (True, x)) ds2)
78+
79+ inferred <- forM tys $ \(shouldGeneralize, (ident, (val, ty))) -> do
80+ -- Replace type class dictionary placeholders with actual dictionaries
81+ (val', unsolved) <- replaceTypeClassDictionaries shouldGeneralize val
82+ -- Generalize and constrain the type
83+ currentSubst <- gets checkSubstitution
84+ let ty' = substituteType currentSubst ty
85+ unsolvedTypeVars = nub $ unknownsInType ty'
86+ generalized = generalize unsolved ty'
87+
88+ when shouldGeneralize $ do
89+ -- Show the inferred type in a warning
90+ tell . errorMessage $ MissingTypeDeclaration ident generalized
91+ -- For non-recursive binding groups, can generalize over constraints.
92+ -- For recursive binding groups, we throw an error here for now.
93+ when (bindingGroupType == RecursiveBindingGroup && not (null unsolved))
94+ . throwError
95+ . errorMessage
96+ $ CannotGeneralizeRecursiveFunction ident generalized
97+ -- Make sure any unsolved type constraints only use type variables which appear
98+ -- unknown in the inferred type.
99+ forM_ unsolved $ \(_, con) -> do
100+ -- We need information about functional dependencies, since we allow
101+ -- ambiguous types to be inferred if they can be solved by some functional
102+ -- dependency.
103+ let findClass = fromMaybe (internalError "entails: type class not found in environment") . M.lookup (constraintClass con)
104+ TypeClassData{ typeClassDependencies } <- gets (findClass . typeClasses . checkEnv)
105+ let solved = foldMap (S.fromList . fdDetermined) typeClassDependencies
106+ let constraintTypeVars = nub . foldMap (unknownsInType . fst) . filter ((`notElem` solved) . snd) $ zip (constraintArgs con) [0..]
107+ when (any (`notElem` unsolvedTypeVars) constraintTypeVars) $
108+ throwError . onErrorMessages (replaceTypes currentSubst) . errorMessage $ NoInstanceFound con
109+
110+ -- Check skolem variables did not escape their scope
111+ skolemEscapeCheck val'
112+ -- Check rows do not contain duplicate labels
113+ checkDuplicateLabels val'
114+ return (ident, (foldr (Abs . Left . fst) val' unsolved, generalized))
115+
116+ -- Show warnings here, since types in wildcards might have been solved during
117+ -- instance resolution (by functional dependencies).
118+ finalSubst <- gets checkSubstitution
119+ escalateWarningWhen isHoleError . tell . onErrorMessages (replaceTypes finalSubst) $ w
120+
121+ return inferred
106122 where
123+ replaceTypes subst = onTypesInErrorMessage (substituteType subst)
107124
108− -- | Generalize type vars using forall and add inferred constraints
109− generalize unsolved = varIfUnknown . constrain unsolved
125+ -- | Generalize type vars using forall and add inferred constraints
126+ generalize unsolved = varIfUnknown . constrain unsolved
110127
111− -- | Add any unsolved constraints
112− constrain [] = id
113− constrain cs = ConstrainedType (map snd cs)
128+ -- | Add any unsolved constraints
129+ constrain [] = id
130+ constrain cs = ConstrainedType (map snd cs)
114131
115− -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
116− tidyUp (ts, sub) = map (\(b, (i, (val, ty))) -> (b, (i, (overTypes (substituteType sub) val, substituteType sub ty)))) ts
132+ -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
133+ tidyUp ts sub = map (\(b, (i, (val, ty))) -> (b, (i, (overTypes (substituteType sub) val, substituteType sub ty)))) ts
117134
118− -- Replace all the wildcards types with their inferred types
119− replace sub = onTypesInErrorMessage (substituteType sub)
120−
121− isHoleError :: ErrorMessage -> Bool
122− isHoleError (ErrorMessage _ HoleInferredType{}) = True
123− isHoleError _ = False
135+ isHoleError :: ErrorMessage -> Bool
136+ isHoleError (ErrorMessage _ HoleInferredType{}) = True
137+ isHoleError _ = False
124138
125139type TypeData = M.Map (Qualified Ident) (Type, NameKind, NameVisibility)
126140
@@ -526,26 +540,6 @@ check' val t@(ConstrainedType constraints ty) = do
526540 dicts <- join <$> zipWithM (newDictionaries []) (map (Qualified Nothing) dictNames) constraints
527541 val' <- withBindingGroupVisible $ withTypeClassDictionaries dicts $ check val ty
528542 return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
529− where
530− -- | Add a dictionary for the constraint to the scope, and dictionaries
531− -- for all implied superclass instances.
532− newDictionaries
533− :: [(Qualified (ProperName 'ClassName), Integer)]
534− -> Qualified Ident
535− -> Constraint
536− -> m [TypeClassDictionaryInScope]
537− newDictionaries path name (Constraint className instanceTy _) = do
538− tcs <- gets (typeClasses . checkEnv)
539− let (args, _, superclasses) = fromMaybe (internalError "newDictionaries: type class lookup failed") $ M.lookup className tcs
540− supDicts <- join <$> zipWithM (\(Constraint supName supArgs _) index ->
541− newDictionaries ((supName, index) : path)
542− name
543− (Constraint supName (instantiateSuperclass (map fst args) supArgs instanceTy) Nothing)
544− ) superclasses [0..]
545− return (TypeClassDictionaryInScope name path className instanceTy Nothing : supDicts)
546−
547− instantiateSuperclass :: [String] -> [Type] -> [Type] -> [Type]
548− instantiateSuperclass args supArgs tys = map (replaceAllTypeVars (zip args tys)) supArgs
549543check' val u@(TUnknown _) = do
550544 val'@(TypedValue _ _ ty) <- infer val
551545 -- Don't unify an unknown with an inferred polytype
src/Language/PureScript/TypeChecker/Unify.hs+1−31
@@ -10,7 +10,6 @@ module Language.PureScript.TypeChecker.Unify
1010 , unknownsInType
1111 , unifyTypes
1212 , unifyRows
13− , unifiesWith
1413 , replaceVarWithUnknown
1514 , replaceTypeWildcards
1615 , varIfUnknown
@@ -102,6 +101,7 @@ unifyTypes t1 t2 = do
102101 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
103102 unifyTypes' ty1@(TypeConstructor c1) ty2@(TypeConstructor c2) =
104103 guardWith (errorMessage (TypesDoNotUnify ty1 ty2)) (c1 == c2)
104+ unifyTypes' (TypeLevelString s1) (TypeLevelString s2) | s1 == s2 = return ()
105105 unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do
106106 t3 `unifyTypes` t5
107107 t4 `unifyTypes` t6
@@ -152,36 +152,6 @@ unifyRows r1 r2 =
152152 unifyRows' _ _ _ _ =
153153 throwError . errorMessage $ TypesDoNotUnify r1 r2
154154
155−-- |
156−-- Check that two types unify
157−--
158−unifiesWith :: Type -> Type -> Bool
159−unifiesWith (TUnknown u1) (TUnknown u2) = u1 == u2
160−unifiesWith (Skolem _ s1 _ _) (Skolem _ s2 _ _) = s1 == s2
161−unifiesWith (TypeVar v1) (TypeVar v2) = v1 == v2
162−unifiesWith (TypeLevelString s1) (TypeLevelString s2) = s1 == s2
163−unifiesWith (TypeConstructor c1) (TypeConstructor c2) = c1 == c2
164−unifiesWith (TypeApp h1 t1) (TypeApp h2 t2) = h1 `unifiesWith` h2 && t1 `unifiesWith` t2
165−unifiesWith REmpty REmpty = True
166−unifiesWith r1@RCons{} r2@RCons{} =
167− let (s1, r1') = rowToList r1
168− (s2, r2') = rowToList r2
169−
170− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
171− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
172− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
173− in all (uncurry unifiesWith) int && go sd1 r1' sd2 r2'
174− where
175− go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
176− go [] REmpty [] REmpty = True
177− go [] (TypeVar v1) [] (TypeVar v2) = v1 == v2
178− go [] (Skolem _ s1 _ _) [] (Skolem _ s2 _ _) = s1 == s2
179− go [] (TUnknown _) _ _ = True
180− go _ _ [] (TUnknown _) = True
181− go _ (TUnknown _) _ (TUnknown _) = True
182− go _ _ _ _ = False
183−unifiesWith _ _ = False
184−
185155-- |
186156-- Replace a single type variable with a new unification variable
187157--
src/Language/PureScript/TypeClassDictionaries.hs−23
@@ -22,26 +22,3 @@ data TypeClassDictionaryInScope
2222 , tcdDependencies :: Maybe [Constraint]
2323 }
2424 deriving (Show)
25−
26−-- |
27−-- A simplified representation of expressions which are used to represent type
28−-- class dictionaries at runtime, which can be compared for equality
29−--
30−data DictionaryValue
31− -- |
32− -- A dictionary which is brought into scope by a local constraint
33− --
34− = LocalDictionaryValue (Qualified Ident)
35− -- |
36− -- A dictionary which is brought into scope by an instance declaration
37− --
38− | GlobalDictionaryValue (Qualified Ident)
39− -- |
40− -- A dictionary which depends on other dictionaries
41− --
42− | DependentDictionaryValue (Qualified Ident) [DictionaryValue]
43− -- |
44− -- A subclass dictionary
45− --
46− | SubclassDictionaryValue DictionaryValue (Qualified (ProperName 'ClassName)) Integer
47− deriving (Show, Ord, Eq)
tests/Language/PureScript/Ide/SourceFileSpec.hs+2−2
@@ -17,8 +17,8 @@ typeAnnotation1, value1, synonym1, class1, class2, data1, data2, foreign1, forei
1717typeAnnotation1 = P.TypeDeclaration (P.Ident "value1") P.REmpty
1818value1 = P.ValueDeclaration (P.Ident "value1") P.Public [] (Left [])
1919synonym1 = P.TypeSynonymDeclaration (P.ProperName "Synonym1") [] P.REmpty
20−class1 = P.TypeClassDeclaration (P.ProperName "Class1") [] [] []
21−class2 = P.TypeClassDeclaration (P.ProperName "Class2") [] []
20+class1 = P.TypeClassDeclaration (P.ProperName "Class1") [] [] [] []
21+class2 = P.TypeClassDeclaration (P.ProperName "Class2") [] [] []
2222 [P.PositionedDeclaration span2 [] member1]
2323data1 = P.DataDeclaration P.Newtype (P.ProperName "Data1") [] []
2424data2 = P.DataDeclaration P.Data (P.ProperName "Data2") [] [(P.ProperName "Cons1", [])]