6954b06 · rowtype-yoga/purescript-native

examples/failing/RowInInstanceNotDetermined0.pursnew file+9

compare with golang

unifiedsplit

@@ -0,0 +1,9 @@

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

3+

4+import Prelude

5+

6+-- no fundeps

7+class C a b

8+instance c :: C Unit {}

9+

examples/failing/RowInInstanceNotDetermined1.pursnew file+9

@@ -0,0 +1,9 @@

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

3+

4+import Prelude

5+

6+-- `c` not mentioned in any fundeps

7+class C a b c | a -> b

8+instance c :: C Unit Unit {}

9+

examples/failing/RowInInstanceNotDetermined2.pursnew file+9

@@ -0,0 +1,9 @@

1+-- @shouldFailWith InvalidInstanceHead

2+module Main where

3+

4+import Prelude

5+

6+-- `b` isn't determined by anything that `b` doesn't determine

7+class C a b | a -> b, b -> a

8+instance c :: C Unit {}

9+

examples/passing/RowInInstanceHeadDetermined.pursnew file+40

@@ -0,0 +1,40 @@

1+module Main where

2+

3+import Prelude

4+import Control.Monad.Eff.Console (log)

5+

6+data Empty = Empty

7+data Cons = Cons

8+

9+

10+-- simple case

11+class Simple a b | a -> b where c :: a -> b

12+instance simple0 :: Simple Empty {} where c _ = {}

13+instance simple1 :: Simple Cons {foo :: Cons} where c cons = {foo: cons}

14+

15+

16+-- simple transitive example

17+class Transitive a b c | a -> b, b -> c where d :: a -> c

18+instance transitive :: Transitive Empty {} {} where d _ = {}

19+

20+

21+-- transitive example with cycles

22+class Cyclic a b c d | a -> b, b -> a

23+ , a -> c

24+ , c -> d, d -> c

25+instance cyclic :: Cyclic Empty Empty {} {}

26+

27+

28+-- Determined cycle

29+class DeterminedCycle a b c | a -> b

30+ , b -> c, c -> b

31+instance determinedCycle :: DeterminedCycle Empty {} {}

32+

33+

34+-- multiple determiners

35+class MultipleDeterminers a b c d | a b -> c d

36+instance multipleDeterminers :: MultipleDeterminers Empty Empty {} {}

37+

38+

39+main = log "Done"

40+

src/Language/PureScript/Environment.hs+53−2

@@ -7,9 +7,12 @@ import Prelude.Compat

7import Data.Aeson.TH

8import qualified Data.Aeson as A

9import qualified Data.Map as M

10+import qualified Data.Set as S

10import Data.Maybe (fromMaybe)

11import Data.Maybe (fromMaybe)

11import Data.Text (Text)

12import Data.Text (Text)

12import qualified Data.Text as T

13import qualified Data.Text as T

14+import Data.List (nub)

15+import qualified Data.Graph as G

13

16

14import Language.PureScript.Crash

17import Language.PureScript.Crash

15import Language.PureScript.Kinds

18import Language.PureScript.Kinds

@@ -48,6 +51,10 @@ data TypeClassData = TypeClassData

48 -- are considered bound in the types appearing in these constraints.

51 -- are considered bound in the types appearing in these constraints.

49 , typeClassDependencies :: [FunctionalDependency]

52 , typeClassDependencies :: [FunctionalDependency]

50 -- ^ A list of functional dependencies for the type arguments of this class.

53 -- ^ A list of functional dependencies for the type arguments of this class.

54+ , typeClassDeterminedArguments :: S.Set Int

55+ -- ^ A set of indexes of type argument that are fully determined by other

56+ -- arguments via functional dependencies. This can be computed from both

57+ -- typeClassArguments and typeClassDependencies.

51 } deriving Show

58 } deriving Show

52

59

53-- | A functional dependency indicates a relationship between two sets of

60-- | A functional dependency indicates a relationship between two sets of

@@ -65,6 +72,50 @@ data FunctionalDependency = FunctionalDependency

65initEnvironment :: Environment

72initEnvironment :: Environment

66initEnvironment = Environment M.empty primTypes M.empty M.empty M.empty primClasses

73initEnvironment = Environment M.empty primTypes M.empty M.empty M.empty primClasses

67

74

75+-- |

76+-- A constructor for TypeClassData that computes which type class arguments are fully determined.

77+-- Fully determined means that this argument cannot be used when selecting a type class instance.

78+--

79+-- An example of the difference between determined and fully determined would be with the class:

80+-- ```class C a b c | a -> b, b -> a, b -> c```

81+-- In this case, `a` must differ when `b` differs, and vice versa - each is determined by the other.

82+-- Both `a` and `b` can be used in selecting a type class instance. However, `c` cannot - it is

83+-- fully determined by `a` and `b`.

84+--

85+-- Define a graph of type class arguments with edges being fundep determiners to determined.

86+-- An argument is fully determined if doesn't appear at the start of a path of strongly connected components.

87+-- An argument is not fully determined otherwise.

88+--

89+-- The way we compute this is by saying: an argument X is fully determined if there are arguments that

90+-- determine X that X does not determine. This is the same thing: everything X determines includes everything

91+-- in its SCC, and everything determining X is either before it in an SCC path, or in the same SCC.

92+makeTypeClassData

93+ :: [(Text, Maybe Kind)]

94+ -> [(Ident, Type)]

95+ -> [Constraint]

96+ -> [FunctionalDependency]

97+ -> TypeClassData

98+makeTypeClassData args m s deps = TypeClassData args m s deps determinedArgs

99+ where

100+ -- list all the edges in the graph: for each fundep an edge exists for each determiner to each determined

101+ contributingDeps = M.fromListWith (++) $ do

102+ fd <- deps

103+ src <- fdDeterminers fd

104+ (src, fdDetermined fd) : map (, []) (fdDetermined fd)

105+

106+ -- here we build a graph of which arguments determine other arguments

107+ (depGraph, _, fromKey) = G.graphFromEdges ((\(n, v) -> (n, n, nub v)) <$> M.toList contributingDeps)

108+

109+ -- do there exist any arguments that contribute to `arg` that `arg` doesn't contribute to

110+ isFunDepDetermined arg = case fromKey arg of

111+ Nothing -> False -- not mentioned in fundeps

112+ Just v -> let contributesToVar = G.reachable (G.transposeG depGraph) v

113+ varContributesTo = G.reachable depGraph v

114+ in any (\r -> not (r `elem` varContributesTo)) contributesToVar

115+

116+ -- find all the arguments that are determined

117+ determinedArgs = S.fromList $ filter isFunDepDetermined [0 .. length args - 1]

118+

68-- |

119-- |

69-- The visibility of a name in scope

120-- The visibility of a name in scope

70--

121--

@@ -264,8 +315,8 @@ primTypes =

264primClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData

315primClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData

265primClasses =

316primClasses =

266 M.fromList

317 M.fromList

267− [ (primName "Partial", (TypeClassData [] [] [] []))

318+ [ (primName "Partial", (makeTypeClassData [] [] [] []))

268− , (primName "Fail", (TypeClassData [("message", Just Symbol)] [] [] []))

319+ , (primName "Fail", (makeTypeClassData [("message", Just Symbol)] [] [] []))

269 ]

320 ]

270

321

271-- |

322-- |

src/Language/PureScript/Errors.hs+1−1

@@ -726,7 +726,7 @@ prettyPrintSingleError (PPEOptions codeColor full level showWiki) e = flip evalS

726 renderSimpleErrorMessage (InvalidInstanceHead ty) =

727 paras [ line "Type class instance head is invalid due to use of type"

728 , markCodeBox $ indent $ typeAsBox ty

729− , line "All types appearing in instance declarations must be of the form T a_1 .. a_n, where each type a_i is of the same form."

729+ , line "All types appearing in instance declarations must be of the form T a_1 .. a_n, where each type a_i is of the same form, unless the type is fully determined by other type class arguments via functional dependencies."

730 ]

731 renderSimpleErrorMessage (TransitiveExportError x ys) =

732 paras [ line $ "An export for " <> markCode (prettyPrintExport x) <> " requires the following to also be exported: "

src/Language/PureScript/Externs.hs+1−1

@@ -144,7 +144,7 @@ applyExternsFileToEnvironment ExternsFile{..} = flip (foldl' applyDecl) efDeclar

144 applyDecl env (EDTypeSynonym pn args ty) = env { typeSynonyms = M.insert (qual pn) (args, ty) (typeSynonyms env) }

145 applyDecl env (EDDataConstructor pn dTy tNm ty nms) = env { dataConstructors = M.insert (qual pn) (dTy, tNm, ty, nms) (dataConstructors env) }

146 applyDecl env (EDValue ident ty) = env { names = M.insert (Qualified (Just efModuleName) ident) (ty, External, Defined) (names env) }

147− applyDecl env (EDClass pn args members cs deps) = env { typeClasses = M.insert (qual pn) (TypeClassData args members cs deps) (typeClasses env) }

147+ applyDecl env (EDClass pn args members cs deps) = env { typeClasses = M.insert (qual pn) (makeTypeClassData args members cs deps) (typeClasses env) }

148 applyDecl env (EDInstance className ident tys cs) = env { typeClassDictionaries = updateMap (updateMap (M.insert (qual ident) dict) className) (Just efModuleName) (typeClassDictionaries env) }

149 where

150 dict :: NamedDict

src/Language/PureScript/Sugar/TypeClasses.hs+2−6

@@ -57,11 +57,7 @@ desugarTypeClasses externs = flip evalStateT initialState . traverse desugarModu

57 -> ExternsDeclaration

58 -> Maybe ((ModuleName, ProperName 'ClassName), TypeClassData)

59 fromExternsDecl mn (EDClass name args members implies deps) = Just ((mn, name), typeClass) where

60− typeClass = TypeClassData { typeClassArguments = args

60+ typeClass = makeTypeClassData args members implies deps

61− , typeClassMembers = members

62− , typeClassSuperclasses = implies

63− , typeClassDependencies = deps

64− }

65 fromExternsDecl _ _ = Nothing

61 fromExternsDecl _ _ = Nothing

66

62

67desugarModule

63desugarModule

@@ -182,7 +178,7 @@ desugarDecl

182desugarDecl mn exps = go

178desugarDecl mn exps = go

183 where

179 where

184 go d@(TypeClassDeclaration name args implies deps members) = do

180 go d@(TypeClassDeclaration name args implies deps members) = do

185− modify (M.insert (mn, name) (TypeClassData args (map memberToNameAndType members) implies deps))

181+ modify (M.insert (mn, name) (makeTypeClassData args (map memberToNameAndType members) implies deps))

186 return (Nothing, d : typeClassDictionaryDeclaration name args implies members : map (typeClassMemberToDictionaryAccessor mn name args) members)

182 return (Nothing, d : typeClassDictionaryDeclaration name args implies members : map (typeClassMemberToDictionaryAccessor mn name args) members)

187 go (TypeInstanceDeclaration _ _ _ _ DerivedInstance) = internalError "Derived instanced should have been desugared"

183 go (TypeInstanceDeclaration _ _ _ _ DerivedInstance) = internalError "Derived instanced should have been desugared"

188 go d@(TypeInstanceDeclaration name deps className tys (ExplicitInstance members)) = do

184 go d@(TypeInstanceDeclaration name deps className tys (ExplicitInstance members)) = do

src/Language/PureScript/TypeChecker.hs+32−22

@@ -22,6 +22,7 @@ import Data.Foldable (for_, traverse_)

22import Data.List (nub, nubBy, (\\), sort, group)

23import Data.Maybe

24import qualified Data.Map as M

25+import qualified Data.Set as S

25import Data.Monoid ((<>))

26import Data.Monoid ((<>))

26import qualified Data.Text as T

27import qualified Data.Text as T

27import Data.Text (Text)

28import Data.Text (Text)

@@ -124,12 +125,7 @@ addTypeClass moduleName pn args implies dependencies ds =

124 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) newClass (typeClasses . checkEnv $ st) } }

125 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) newClass (typeClasses . checkEnv $ st) } }

125 where

126 where

126 newClass :: TypeClassData

127 newClass :: TypeClassData

127− newClass =

128+ newClass = makeTypeClassData args (map toPair ds) implies dependencies

128− TypeClassData { typeClassArguments = args

129− , typeClassMembers = map toPair ds

130− , typeClassSuperclasses = implies

131− , typeClassDependencies = dependencies

132− }

133

129

134 toPair (TypeDeclaration ident ty) = (ident, ty)

130 toPair (TypeDeclaration ident ty) = (ident, ty)

135 toPair (PositionedDeclaration _ _ d) = toPair d

131 toPair (PositionedDeclaration _ _ d) = toPair d

@@ -155,18 +151,28 @@ checkDuplicateTypeArguments args = for_ firstDup $ \dup ->

155 firstDup = listToMaybe $ args \\ nub args

151 firstDup = listToMaybe $ args \\ nub args

156

152

157checkTypeClassInstance

153checkTypeClassInstance

158− :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)

154+ :: (MonadState CheckState m, MonadError MultipleErrors m)

159− => ModuleName

155+ => TypeClassData

156+ -> Int -- ^ index of type class argument

160 -> Type

157 -> Type

161 -> m ()

158 -> m ()

162−checkTypeClassInstance _ (TypeVar _) = return ()

159+checkTypeClassInstance cls i = check where

160+ -- If the argument is determined via fundeps then we are less restrictive in

161+ -- what type is allowed. This is because the type cannot be used to influence

162+ -- which instance is selected. Currently the only weakened restriction is that

163+ -- row types are allowed in determined type class arguments.

164+ isFunDepDetermined = S.member i (typeClassDeterminedArguments cls)

165+ check = \case

166+ TypeVar _ -> return ()

163−checkTypeClassInstance _ (TypeLevelString _) = return ()

167+ TypeLevelString _ -> return ()

164−checkTypeClassInstance _ (TypeConstructor ctor) = do

168+ TypeConstructor ctor -> do

165− env <- getEnv

169+ env <- getEnv

166− when (ctor `M.member` typeSynonyms env) . throwError . errorMessage $ TypeSynonymInstance

170+ when (ctor `M.member` typeSynonyms env) . throwError . errorMessage $ TypeSynonymInstance

167− return ()

171+ return ()

168−checkTypeClassInstance m (TypeApp t1 t2) = checkTypeClassInstance m t1 >> checkTypeClassInstance m t2

172+ TypeApp t1 t2 -> check t1 >> check t2

173+ REmpty | isFunDepDetermined -> return ()

174+ RCons _ hd tl | isFunDepDetermined -> check hd >> check tl

169−checkTypeClassInstance _ ty = throwError . errorMessage $ InvalidInstanceHead ty

175+ ty -> throwError . errorMessage $ InvalidInstanceHead ty

170

176

171-- |

177-- |

172-- Check that type synonyms are fully-applied in a type

178-- Check that type synonyms are fully-applied in a type

@@ -283,12 +289,16 @@ typeCheckAll moduleName _ = traverse go

283 addTypeClass moduleName pn args implies deps tys

289 addTypeClass moduleName pn args implies deps tys

284 return d

290 return d

285 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do

291 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do

292+ env <- getEnv

293+ case M.lookup className (typeClasses env) of

294+ Nothing -> internalError "typeCheckAll: Encountered unknown type class in instance declaration"

295+ Just typeClass -> do

286− traverse_ (checkTypeClassInstance moduleName) tys

296+ sequence_ (zipWith (checkTypeClassInstance typeClass) [0..] tys)

287− checkOrphanInstance dictName className tys

297+ checkOrphanInstance dictName className tys

288− _ <- traverseTypeInstanceBody checkInstanceMembers body

298+ _ <- traverseTypeInstanceBody checkInstanceMembers body

289− let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)

299+ let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)

290− addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (tcdValue dict) dict

300+ addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (tcdValue dict) dict

291− return d

301+ return d

292 go (PositionedDeclaration pos com d) =

302 go (PositionedDeclaration pos com d) =

293 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d

303 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d

294

304