[started implementing type inference mail@stefanwehr.de**20050520082619] { hunk ./Entailment.hs 7 --- entails :: [ClassConstraint +--entails :: [ConstraintScheme] hunk ./Error.hs 29 - debug_ + debug_, enableDebug hunk ./Error.hs 35 - +import Data.IORef hunk ./Error.hs 130 - in liftIO (putStrLn s) + in do f <- liftIO $ readIORef debugFlag + if f then liftIO (putStrLn s) else return () hunk ./Error.hs 140 +enableDebug :: IO () +enableDebug = + writeIORef debugFlag True hunk ./Error.hs 144 +debugFlag :: IORef Bool +debugFlag = unsafePerformIO (newIORef False) +{-# NOINLINE debugFlag #-} hunk ./KindInference.hs 48 +kindApps' :: [Kind'] -> Kind' -> Kind' +kindApps' args result = + foldr Kfun result args + hunk ./KindInference.hs 334 - do debug ("kiClassHead: " ++ show name) - varKind <- newKindVar + do varKind <- newKindVar hunk ./KindInference.hs 341 - let typeDefKind = foldr Kfun Star argKinds + let typeDefKind = kindApps' argKinds Star hunk ./KindInference.hs 370 - let assocTypeKind = foldr Kfun resultKind (indexKind:restKinds) + let assocTypeKind = kindApps' (indexKind:restKinds) resultKind hunk ./KindInference.hs 409 - unify atKind (foldr Kfun resKind (indexKind:paramKinds)) + unify atKind (kindApps' (indexKind:paramKinds) resKind) hunk ./KindInference.hs 444 - unify k (foldr Kfun resultKind paramKinds) + unify k (kindApps' paramKinds resultKind) hunk ./Kinds.hs 27 - return $ foldr KindFun KindStar paramKinds + return $ kindApps paramKinds KindStar hunk ./Kinds.hs 32 - return $ foldr KindFun KindStar paramKinds + return $ kindApps paramKinds KindStar hunk ./Main.hs 85 + when (on Debug) enableDebug + hunk ./Main.hs 144 + | Debug hunk ./Main.hs 176 - + , Option [] ["debug"] (NoArg Debug) "enable debug messages" hunk ./ParseSyntax.hs 132 +kindApps :: [Kind] -> Kind -> Kind +kindApps args result = + foldr KindFun result args + hunk ./ParseSyntax.hs 143 +tyApps :: [Type] -> Type -> Type +tyApps args result = + foldr TyApp result args hunk ./ParseSyntax.hs 158 - = TypeScheme [TypeVarId] QualifiedType + = TypeScheme { tyscheme_quants :: [TypeVarId], + tyscheme_qtype :: QualifiedType + } hunk ./Pretty.hs 23 - printDoc, showPpr, + printDoc, showPpr, showList, showCommaListed, hunk ./Pretty.hs 63 + +pprList :: Pretty p => String -> [p] -> Doc +pprList delim l = + hcat $ punctuate (text delim) (map ppr l) + +showCommaListed :: Pretty p => [p] -> String +showCommaListed l = + show $ pprList ", " l hunk ./Substitution.hs 9 - mergeSubst, substLookup, substFromAssocs, instantiateScheme + mergeSubst, substLookup, substFromAssocs, hunk ./Substitution.hs 12 +import qualified Map hunk ./Substitution.hs 34 - + +instance Substitution a b c => Substitution a b (Map.Map k c) where + applySubst s m = Map.map (applySubst s) m + hunk ./Substitution.hs 87 -instantiateScheme :: Substitution a b c => [a] -> [b] -> c -> c -instantiateScheme as bs c = - applySubst (substFromAssocs (zip as bs)) c + hunk ./Symtab.hs 1 +{-# OPTIONS_GHC -fglasgow-exts #-} +-- for "Non-type variables in constraint" + hunk ./Symtab.hs 15 - freshTypeVar, freshTypeVars + instantiate, freshTypeVar hunk ./Symtab.hs 27 +import Substitution hunk ./Symtab.hs 107 -freshTypeVar :: ST TypeVarId -freshTypeVar = +-- we return a Type instead of a TypeVarId here, because it eliminates +-- the risk of instantiating a type scheme "the wrong way round" (replacing +-- the fresh vars with the quantified vars). + +instantiate :: Substitution TypeVarId Type c => + [TypeVarId] -> c -> ST (c, [TypeVarId]) +instantiate quants c = + do kinds <- mapM kindOfTypeVarId quants + freshs <- mapM freshTypeVar' kinds + let subst = substFromAssocs (zip quants (map TyVar freshs)) + return (applySubst subst c, freshs) + +freshTypeVar' :: Kind -> ST TypeVarId +freshTypeVar' k = hunk ./Symtab.hs 123 - return (UniqIdents.mkTypeVar "v" cur) + let id = UniqIdents.mkTypeVar "v" cur + insertKind id k + return id hunk ./Symtab.hs 127 -freshTypeVars :: Int -> ST [TypeVarId] -freshTypeVars n = - mapM (\_ -> freshTypeVar) [1..n] +freshTypeVar :: Kind -> ST Type +freshTypeVar k = + do id <- freshTypeVar' k + return (TyVar id) hunk ./Unification.hs 66 + deriving (Show) hunk ./Unification.hs 68 +instance Pretty TypeEq where + pprPrec prec (t1 :=: t2) = + parens `usedWhen` (prec > minPrec) $ + ppr t1 <+> text "=" <+> ppr t2 + hunk ./Unification.hs 77 - (map (\ (t1 :=: t2) -> showPpr t1 ++ " = " ++ showPpr t2) eqs) + (map showPpr eqs) hunk ./Unification.hs 83 -data UFState = UFState { uf_theta :: [ConstraintScheme] } +type InstanceEnv = [ConstraintScheme] hunk ./Unification.hs 85 +data UFState = UFState { uf_theta :: InstanceEnv } + +-- FIXME: type UFResult = ([EqConstraint], TypeSubst) hunk ./Unification.hs 95 -runUF :: [ConstraintScheme] -> UF a -> ST a +runUF :: InstanceEnv -> UF a -> ST a hunk ./Unification.hs 139 - reduceAT id params (EqScheme quant eq : rest) = + reduceAT id params (EqScheme quants eq : rest) = hunk ./Unification.hs 143 - freshs <- freshTypeVars (length quant) - let eq' = instantiateScheme quant (map TyVar freshs) eq + (eq', freshs) <- instantiate quants eq hunk ./Unification.hs 147 - subst <- matchTypes freshs (assoc_params . eqc_left $ eq') - params + subst <- matchTypes freshs + (assoc_params . eqc_left $ eq') params hunk ./Unification.hs 203 -unify :: [TypeEq] -> UF UFResult +unify :: [TypeEq] -> UF ([EqConstraint], TypeSubst) hunk ./Unification.hs 205 + do debug ("running unification on " ++ showEqs eqs) + (u, r) <- unify' eqs + -- u should only contain constraints of the form `T t1 = t2' where + -- T is an associated type synonym and t2 is not a type variable. + -- Unsatisfiable constraints (like `Int = Bool') signal unification + -- failure + let u' = map adjustConstraint u + debug ("unification finished, substitution: " ++ showSubst r ++ + "\n pending equality constraints: " ++ showCommaListed u') + return (u', r) + where adjustConstraint (t :=: TyAssoc at) = + adjustConstraint (TyAssoc at :=: t) + adjustConstraint c@(TyAssoc at :=: t) = + case t of + TyVar _ -> panic ("Equality constraint `" ++ showPpr c ++ + "' in result when unifying " ++ + showEqs eqs) + _ -> EqConstraint at t + adjustConstraint c@(t1 :=: t2) = + failwith UnificationFailed + ("Cannot unify " ++ showEqs eqs ++ + ". Unsatisfiable equality constraint: " ++ showPpr c) + +unify' :: [TypeEq] -> UF UFResult +unify' eqs = hunk ./Unification.hs 234 - do (u'',r'') <- unify ((applySubst r' u) ++ u') + do (u'',r'') <- unify' ((applySubst r' u) ++ u') hunk ./WellFormedProgram.hs 58 - in do debug ("unifying `" ++ showPpr t1 ++ "' with `" ++ - showPpr t2 ++ "'") - (eqs, subst) <- runUF [] (unify [t1 :=: t2]) - debug ("Substitution: " ++ showSubst subst) - debug ("Pending equalities: " ++ showEqs eqs) - return False + in catchST (tryUnify t1 t2) + [UnificationFailed] (\_ -> return False) + tryUnify t1 t2 = + do (eqc, _) <- runUF [] (unify [t1 :=: t2]) + if null eqc then return True + else panic + ("Unification succeeded with the following equality " + ++ "constraints when checking for overlapping " + ++ "instances: " ++ showCommaListed eqc) }