5d19bd9 · rowtype-yoga/purescript-native

git.iko.soy/rowtype-yoga/purescript-native

Fix issue with type variables in super class dictionary types. Simplify desugaring somewhat, add more examples

commit5d19bd9580907e2073e52faf8a905946434d559d authorPhil Freeman <paf31@cantab.net> dateSun 6 Apr 2014, 12:44 (13 years ago) parenta8108d0

7 files changed+107−40

compare with golang

unifiedsplit

examples/failing/Superclasses2.purs+9 examples/failing/Superclasses3.purs+5 examples/passing/EqOrd.purs+14 src/Language/PureScript/Declarations.hs+5−1 src/Language/PureScript/Pretty/Values.hs+1 src/Language/PureScript/Sugar/TypeClasses.hs+30−22 src/Language/PureScript/TypeChecker/Types.hs+43−17

examples/failing/Superclasses2.pursnew file+9

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

1+module CycleInSuperclasses where

3+class (Foo a) <= Bar a

5+class (Bar a) <= Foo a

7+instance barString :: Bar String

9+instance fooString :: Foo String

examples/failing/Superclasses3.pursnew file+5

@@ -0,0 +1,5 @@

1+module UnknownSuperclassTypeVar where

3+class Foo a

5+class (Foo b) <= Bar a

examples/passing/EqOrd.pursnew file+14

@@ -0,0 +1,14 @@

1+module Main where

3+data Pair a b = Pair a b

5+instance ordPair :: (Ord a, Ord b) => Ord (Pair a b) where

6+ compare (Pair a1 b1) (Pair a2 b2) = case compare a1 a2 of

7+ EQ -> compare b1 b2

8+ r -> r

10+instance eqPair :: (Eq a, Eq b) => Eq (Pair a b) where

11+ (==) (Pair a1 b1) (Pair a2 b2) = a1 == a2 && b1 == b2

12+ (/=) (Pair a1 b1) (Pair a2 b2) = a1 /= a2 || b1 /= b2

13+

14+main = Debug.Trace.print $ Pair 1 2 == Pair 1 2

src/Language/PureScript/Declarations.hs+5−1

@@ -333,7 +333,11 @@ data Value

333333 -- at superclass implementations when searching for a dictionary, the type class name and

334334 -- instance type, and the type class dictionaries in scope.

335335 --

336− | TypeClassDictionary Bool (Qualified ProperName, [Type]) (Maybe [TypeClassDictionaryInScope])

336+ | TypeClassDictionary Bool (Qualified ProperName, [Type]) [TypeClassDictionaryInScope]

337+ -- |

338+ -- A placeholder for a superclass dictionary to be turned into a TypeClassDictionary during typechecking

339+ --

340+ | SuperClassDictionary (Qualified ProperName) [Type]

337341 -- |

338342 -- A value with source position information

339343 --

src/Language/PureScript/Pretty/Values.hs+1

@@ -74,6 +74,7 @@ literals = mkPattern' match

7474 , currentIndent

7575 ]

7676 match (TypeClassDictionary _ _ _) = return "<<dict>>"

77+ match (SuperClassDictionary _ _) = return "<<superclass dict>>"

7778 match (TypedValue _ val _) = prettyPrintValue' val

7879 match (PositionedValue _ val) = prettyPrintValue' val

7980 match _ = mzero

src/Language/PureScript/Sugar/TypeClasses.hs+30−22

@@ -98,19 +98,18 @@ desugarModule _ = error "Exports should have been elaborated in name desugaring"

9898--

9999-- ...

100100--

101−-- subString :: {} -> { __superclasses :: [{}], sub :: String }

101+-- subString :: {} -> { __superclasses :: { "Foo": {} -> Foo String }, sub :: String }

102102-- subString _ = {

103−-- __superclasses: [\<dictionary placeholder to be inserted during type checking\>]

103+-- __superclasses: {

104+-- "Foo": \_ -> <dictionary placeholder to be inserted during type checking\>

105+-- }

104106-- sub: ""

105107-- }

106108--

107−-- Here, the __superclasses property is not typechecked (it is not even well-typed, since its

108−-- entries might be dictionaries of different types).

109−--

110109desugarDecl :: ModuleName -> Declaration -> Desugar (Maybe DeclarationRef, [Declaration])

111−desugarDecl mn d@(TypeClassDeclaration name args _ members) = do

110+desugarDecl mn d@(TypeClassDeclaration name args implies members) = do

112111 modify (M.insert (mn, name) d)

113− return $ (Nothing, d : typeClassDictionaryDeclaration name args members : map (typeClassMemberToDictionaryAccessor mn name args) members)

112+ return $ (Nothing, d : typeClassDictionaryDeclaration name args implies members : map (typeClassMemberToDictionaryAccessor mn name args) members)

114113desugarDecl mn d@(TypeInstanceDeclaration name deps className ty members) = do

115114 desugared <- lift $ desugarCases members

116115 dictDecl <- typeInstanceDictionaryDeclaration name mn deps className ty desugared

@@ -129,9 +128,15 @@ identToProperty :: Ident -> String

129128identToProperty (Ident name) = name

130129identToProperty (Op op) = op

131130

132−typeClassDictionaryDeclaration :: ProperName -> [String] -> [Declaration] -> Declaration

133−typeClassDictionaryDeclaration name args members =

134− TypeSynonymDeclaration name args (TypeApp tyObject $ rowFromList (map (first identToProperty . memberToNameAndType) members, REmpty))

131+typeClassDictionaryDeclaration :: ProperName -> [String] -> [(Qualified ProperName, [Type])] -> [Declaration] -> Declaration

132+typeClassDictionaryDeclaration name args implies members =

133+ let superclassesType = TypeApp tyObject (rowFromList ([ (fieldName, function unit tySynApp)

134+ | (index, (superclass, tyArgs)) <- zip [0..] implies

135+ , let tySynApp = foldl TypeApp (TypeConstructor superclass) tyArgs

136+ , let fieldName = mkSuperclassDictionaryName superclass index

137+ ], REmpty))

138+

139+ in TypeSynonymDeclaration name args (TypeApp tyObject $ rowFromList ((C.__superclasses, superclassesType) : map (first identToProperty . memberToNameAndType) members, REmpty))

135140

136141typeClassMemberToDictionaryAccessor :: ModuleName -> ProperName -> [String] -> Declaration -> Declaration

137142typeClassMemberToDictionaryAccessor mn name args (TypeDeclaration ident ty) =

@@ -142,6 +147,12 @@ typeClassMemberToDictionaryAccessor mn name args (PositionedDeclaration pos d) =

142147 PositionedDeclaration pos $ typeClassMemberToDictionaryAccessor mn name args d

143148typeClassMemberToDictionaryAccessor _ _ _ _ = error "Invalid declaration in type class definition"

144149

150+mkSuperclassDictionaryName :: Qualified ProperName -> Integer -> String

151+mkSuperclassDictionaryName pn index = show pn ++ "_" ++ show index

152+

153+unit :: Type

154+unit = TypeApp tyObject REmpty

155+

145156typeInstanceDictionaryDeclaration :: Ident -> ModuleName -> [(Qualified ProperName, [Type])] -> Qualified ProperName -> [Type] -> [Declaration] -> Desugar Declaration

146157typeInstanceDictionaryDeclaration name mn deps className tys decls = do

147158 m <- get

@@ -152,11 +163,6 @@ typeInstanceDictionaryDeclaration name mn deps className tys decls = do

152163 M.lookup (qualify mn className) m

153164 let instanceTys = map memberToNameAndType tyDecls

154165

155− let superclasses = TypedValue False (ArrayLiteral [ Abs (Left (Ident "_")) (TypeClassDictionary False (superclass, tyArgs) Nothing)

156− | (superclass, suTyArgs) <- implies

157− , let tyArgs = map (replaceAllTypeVars (zip args tys)) suTyArgs

158− ]) (TypeApp tyArray unit)

159−

160166 -- Replace the type arguments with the appropriate types in the member types

161167 let memberTypes = map (second (replaceAllTypeVars (zip args tys))) instanceTys

162168 -- Create values for the type instance members

@@ -166,17 +172,19 @@ typeInstanceDictionaryDeclaration name mn deps className tys decls = do

166172 -- The dictionary itself is an object literal, but for reasons related to recursion, the dictionary

167173 -- must be guarded by at least one function abstraction. For that reason, if the dictionary has no

168174 -- dependencies, we introduce an unnamed function parameter.

169− let (memberTypes', memberNames') =

170− if null implies

171− then (memberTypes, memberNames)

172− else ((Ident C.__superclasses, TypeApp tyArray unit) : memberTypes, (C.__superclasses, superclasses) : memberNames)

173− dictTy = TypeApp tyObject (rowFromList (map (first identToProperty) memberTypes', REmpty))

175+ let superclasses = ObjectLiteral

176+ [ (fieldName, Abs (Left (Ident "_")) (SuperClassDictionary superclass tyArgs))

177+ | (index, (superclass, suTyArgs)) <- zip [0..] implies

178+ , let tyArgs = map (replaceAllTypeVars (zip args tys)) suTyArgs

179+ , let fieldName = mkSuperclassDictionaryName superclass index

180+ ]

181+

182+ let memberNames' = (C.__superclasses, superclasses) : memberNames

183+ dictTy = foldl TypeApp (TypeConstructor className) tys

174184 constrainedTy = quantify (if null deps then function unit dictTy else ConstrainedType deps dictTy)

175185 dict = if null deps then Abs (Left (Ident "_")) (ObjectLiteral memberNames') else ObjectLiteral memberNames'

176186 return $ ValueDeclaration name TypeInstanceDictionaryValue [] Nothing (TypedValue True dict constrainedTy)

177187 where

178− unit :: Type

179− unit = TypeApp tyObject REmpty

180188

181189 memberToNameAndValue :: [(Ident, Type)] -> Declaration -> Desugar (Ident, Value)

182190 memberToNameAndValue tys' d@(ValueDeclaration ident _ _ _ _) = do

src/Language/PureScript/TypeChecker/Types.hs+43−17

@@ -263,8 +263,7 @@ replaceTypeClassDictionaries mn = everywhereM' (mkM go)

263263 where

264264 go (TypeClassDictionary trySuperclasses constraint dicts) = do

265265 env <- getEnv

266− let dicts' = fromMaybe (typeClassDictionaries env) dicts

267− entails env mn dicts' constraint trySuperclasses

266+ entails env mn dicts constraint trySuperclasses

268267 go other = return other

269268

270269-- |

@@ -287,7 +286,7 @@ data DictionaryValue

287286 -- |

288287 -- A subclass dictionary

289288 --

290− | SubclassDictionaryValue DictionaryValue Integer

289+ | SubclassDictionaryValue DictionaryValue (Qualified ProperName) Integer

291290 deriving (Show, Ord, Eq)

292291

293292-- |

@@ -307,12 +306,12 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt

307306 filterModule _ = False

308307

309308 solve context' (className, tys) trySuperclasses =

310− case chooseSimplestDictionaries (go className tys) of

309+ case chooseSimplestDictionaries (go trySuperclasses className tys) of

311310 [] -> throwError . strMsg $ "No instance found for " ++ show className ++ " " ++ unwords (map prettyPrintTypeAtom tys)

312311 [dict] -> return (dictionaryValueToValue dict)

313312 _ -> throwError . strMsg $ "Overlapping instances found for " ++ show className ++ " " ++ unwords (map prettyPrintTypeAtom tys)

314313 where

315− go className' tys' =

314+ go trySuperclasses' className' tys' =

316315 -- Look for regular type instances

317316 [ mkDictionary (canonicalizeDictionary tcd) args

318317 | tcd <- context'

@@ -324,8 +323,8 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt

324323 , args <- solveSubgoals subst (tcdDependencies tcd) ] ++

325324

326325 -- Look for implementations via superclasses

327− [ SubclassDictionaryValue suDict index

328− | trySuperclasses

326+ [ SubclassDictionaryValue suDict superclass index

327+ | trySuperclasses'

329328 , (subclassName, (args, _, implies)) <- M.toList (typeClasses env)

330329 -- Try each superclass

331330 , (index, (superclass, suTyArgs)) <- zip [0..] implies

@@ -334,7 +333,7 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt

334333 -- Make sure the types unify with the types in the superclass implication

335334 , subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' suTyArgs

336335 -- Finally, satisfy the subclass constraint

337− , suDict <- go subclassName (map (applySubst subst . TypeVar) args) ]

336+ , suDict <- go trySuperclasses' subclassName (map (applySubst subst . TypeVar) args) ]

338337

339338 -- Create dictionaries for subgoals which still need to be solved by calling go recursively

340339 -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type

@@ -342,7 +341,7 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt

342341 solveSubgoals :: [(String, Type)] -> Maybe [(Qualified ProperName, [Type])] -> [Maybe [DictionaryValue]]

343342 solveSubgoals _ Nothing = return Nothing

344343 solveSubgoals subst (Just subgoals) = do

345− dict <- mapM (uncurry go . second (map (replaceAllTypeVars subst))) subgoals

344+ dict <- mapM (uncurry (go True) . second (map (replaceAllTypeVars subst))) subgoals

346345 return $ Just dict

347346 -- Make a dictionary from subgoal dictionaries by applying the correct function

348347 mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue

@@ -354,10 +353,9 @@ entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filt

354353 dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName

355354 dictionaryValueToValue (GlobalDictionaryValue fnName) = App (Var fnName) (ObjectLiteral [])

356355 dictionaryValueToValue (DependentDictionaryValue fnName dicts) = foldl App (Var fnName) (map dictionaryValueToValue dicts)

357− dictionaryValueToValue (SubclassDictionaryValue dict index) =

358− App (App (App (Var (Qualified (Just (ModuleName [ProperName C.prelude])) (Ident (C.!!))))

356+ dictionaryValueToValue (SubclassDictionaryValue dict superclassName index) =

357+ App (Accessor (show superclassName ++ "_" ++ show index)

359358 (Accessor C.__superclasses (dictionaryValueToValue dict)))

360− (NumericLiteral (Left index)))

361359 (ObjectLiteral [])

362360 -- Ensure that a substitution is valid

363361 verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]

@@ -500,7 +498,7 @@ instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do

500498instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do

501499 dicts <- getTypeClassDictionaries

502500 (_, ty') <- instantiatePolyTypeWithUnknowns (error "Types under a constraint cannot themselves be constrained") ty

503− return (foldl App val (map (flip (TypeClassDictionary True) (Just dicts)) constraints), ty')

501+ return (foldl App val (map (flip (TypeClassDictionary True) dicts) constraints), ty')

504502instantiatePolyTypeWithUnknowns val ty = return (val, ty)

505503

506504-- |

@@ -624,7 +622,7 @@ infer' (Var var) = do

624622 case ty of

625623 ConstrainedType constraints ty' -> do

626624 dicts <- getTypeClassDictionaries

627− return $ TypedValue True (foldl App (Var var) (map (flip (TypeClassDictionary True) (Just dicts)) constraints)) ty'

625+ return $ TypedValue True (foldl App (Var var) (map (flip (TypeClassDictionary True) dicts) constraints)) ty'

628626 _ -> return $ TypedValue True (Var var) ty

629627infer' v@(Constructor c) = do

630628 env <- getEnv

@@ -646,6 +644,9 @@ infer' (IfThenElse cond th el) = do

646644infer' (Let ds val) = do

647645 (ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer

648646 return $ TypedValue True (Let ds' val') valTy

647+infer' (SuperClassDictionary className tys) = do

648+ dicts <- getTypeClassDictionaries

649+ return $ TypeClassDictionary False (className, tys) dicts

649650infer' (TypedValue checkType val ty) = do

650651 Just moduleName <- checkCurrentModule <$> get

651652 kind <- liftCheck $ kindOf moduleName ty

@@ -783,6 +784,17 @@ newSkolemScope = SkolemScope . runUnknown <$> fresh'

783784skolemize :: String -> Int -> SkolemScope -> Type -> Type

784785skolemize ident sko scope = replaceTypeVars ident (Skolem sko scope)

785786

787+-- |

788+-- This function has one purpose - to skolemize type variables appearing in a

789+-- SuperClassDictionary placeholder. These type variables are somewhat unique since they are the

790+-- only example of scoped type variables.

791+--

792+skolemizeTypesInValue :: String -> Int -> SkolemScope -> Value -> Value

793+skolemizeTypesInValue ident sko scope = everywhere (mkT go)

794+ where

795+ go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)

796+ go other = other

797+

786798-- |

787799-- Introduce skolem scope at every occurence of a ForAll

788800--

@@ -812,7 +824,8 @@ check' val (ForAll ident ty _) = do

812824 scope <- newSkolemScope

813825 sko <- newSkolemConstant

814826 let sk = skolemize ident sko scope ty

815− val' <- check val sk

827+ let skVal = skolemizeTypesInValue ident sko scope val

828+ val' <- check skVal sk

816829 return $ TypedValue True val' (ForAll ident ty (Just scope))

817830check' val t@(ConstrainedType constraints ty) = do

818831 dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do

@@ -858,6 +871,19 @@ check' v@(Var var) ty = do

858871 case v' of

859872 Nothing -> throwError . strMsg $ "Unable to check type subsumption"

860873 Just v'' -> return $ TypedValue True v'' ty'

874+check' (SuperClassDictionary className tys) _ = do

875+ -- |

876+ -- Here, we replace a placeholder for a superclass dictionary with a regular

877+ -- TypeClassDictionary placeholder. The reason we do this is that it is necessary to have the

878+ -- correct super instance dictionaries in scope, and these are not available when the type class

879+ -- declaration gets desugared.

880+ --

881+ -- Note also that the first argument to TypeClassDictionary is False, meaning we _do not_ want

882+ -- to consider superclass instances when searching for this dictionary - doing so might lead

883+ -- to traversing a cycle in the instance graph.

884+ --

885+ dicts <- getTypeClassDictionaries

886+ return $ TypeClassDictionary False (className, tys) dicts

861887check' (TypedValue checkType val ty1) ty2 = do

862888 Just moduleName <- checkCurrentModule <$> get

863889 kind <- liftCheck $ kindOf moduleName ty1

@@ -990,7 +1016,7 @@ checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do

9901016 checkFunctionApplication fn ty arg ret

9911017checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do

9921018 dicts <- getTypeClassDictionaries

993− checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) (Just dicts)) constraints)) fnTy arg ret

1019+ checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) dicts) constraints)) fnTy arg ret

9941020checkFunctionApplication' _ fnTy arg _ = throwError . strMsg $ "Cannot apply a function of type "

9951021 ++ prettyPrintType fnTy

9961022 ++ " to argument " ++ prettyPrintValue arg

@@ -1033,7 +1059,7 @@ subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do

10331059subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do

10341060 dicts <- getTypeClassDictionaries

10351061 _ <- subsumes' Nothing ty1 ty2

1036− return . Just $ foldl App val (map (flip (TypeClassDictionary True) (Just dicts)) constraints)

1062+ return . Just $ foldl App val (map (flip (TypeClassDictionary True) dicts) constraints)

10371063subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject = do

10381064 let

10391065 (ts1, r1') = rowToList r1