From d03e48a77b7f7b03a088b0dbfa26650d2cfd123b Mon Sep 17 00:00:00 2001 From: Runar Bjarnason Date: Thu, 21 Jun 2018 12:49:12 -0400 Subject: [PATCH] Debugging letrec typechecking --- parser-typechecker/src/Unison/ABT.hs | 2 +- parser-typechecker/src/Unison/Term.hs | 2 +- parser-typechecker/src/Unison/TypeVar.hs | 2 +- .../src/Unison/Typechecker/Components.hs | 6 ++-- .../src/Unison/Typechecker/Context.hs | 19 ++++++---- parser-typechecker/src/Unison/Var.hs | 2 +- .../tests/Unison/Test/Typechecker.hs | 35 +++++++++++++++---- 7 files changed, 48 insertions(+), 20 deletions(-) diff --git a/parser-typechecker/src/Unison/ABT.hs b/parser-typechecker/src/Unison/ABT.hs index 279d9b403..bed51aa8c 100644 --- a/parser-typechecker/src/Unison/ABT.hs +++ b/parser-typechecker/src/Unison/ABT.hs @@ -393,7 +393,7 @@ subtract _ t1s t2s = instance (Show1 f, Var v) => Show (Term f v a) where -- annotations not shown showsPrec p (Term _ _ out) = case out of - Var v -> (Text.unpack (Var.shortName v) ++) + Var v -> (show v ++) Cycle body -> showsPrec p body Abs v body -> showParen True $ (Text.unpack (Var.shortName v) ++) . showString ". " . showsPrec p body Tm f -> showsPrec1 p f diff --git a/parser-typechecker/src/Unison/Term.hs b/parser-typechecker/src/Unison/Term.hs index 2a7e1891b..d4e2ae70e 100644 --- a/parser-typechecker/src/Unison/Term.hs +++ b/parser-typechecker/src/Unison/Term.hs @@ -250,7 +250,7 @@ lam'' vs body = foldr lam body vs -- | Smart constructor for let rec blocks. Each binding in the block may -- reference any other binding in the block in its body (including itself), -- and the output expression may also reference any binding in the block. -letRec :: Ord v => [(v,Term v)] -> Term v -> Term v +letRec :: Ord v => [(v, Term' vt v)] -> Term' vt v -> Term' vt v letRec [] e = e letRec bindings e = ABT.cycle (foldr ABT.abs z (map fst bindings)) where diff --git a/parser-typechecker/src/Unison/TypeVar.hs b/parser-typechecker/src/Unison/TypeVar.hs index 3ccc40f8f..dd2676d29 100644 --- a/parser-typechecker/src/Unison/TypeVar.hs +++ b/parser-typechecker/src/Unison/TypeVar.hs @@ -13,7 +13,7 @@ underlying (Universal v) = v underlying (Existential v) = v instance Show v => Show (TypeVar v) where - show (Universal v) = show v + show (Universal v) = "@" ++ show v show (Existential v) = "'" ++ show v instance Var v => Var (TypeVar v) where diff --git a/parser-typechecker/src/Unison/Typechecker/Components.hs b/parser-typechecker/src/Unison/Typechecker/Components.hs index 351e68ad0..c8ae51875 100644 --- a/parser-typechecker/src/Unison/Typechecker/Components.hs +++ b/parser-typechecker/src/Unison/Typechecker/Components.hs @@ -6,7 +6,7 @@ import Data.Maybe import Data.Set (Set) import qualified Data.Set as Set import qualified Unison.ABT as ABT -import Unison.Term (Term) +import Unison.Term (Term') import qualified Unison.Term as Term import Unison.Var (Var) @@ -63,7 +63,7 @@ components' freeVars bs = -- -- Gets rid of the let rec and replaces it with an ordinary `let`, such -- that `id` is suitably generalized. -minimize :: Var v => Term v -> Maybe (Term v) +minimize :: Var v => Term' vt v -> Maybe (Term' vt v) minimize (Term.LetRecNamed' bs e) = case components bs of [_single] -> Nothing cs -> Just $ foldr mklet e cs where @@ -73,5 +73,5 @@ minimize (Term.LetRecNamed' bs e) = case components bs of mklet cycle e = Term.letRec cycle e minimize _ = Nothing -minimize' :: Var v => Term v -> Term v +minimize' :: Var v => Term' vt v -> Term' vt v minimize' term = fromMaybe term (minimize term) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 6b473d914..c1d1e2bd1 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -42,6 +42,7 @@ import qualified Unison.Term as Term import qualified Unison.Type as Type import Unison.TypeVar (TypeVar) import qualified Unison.TypeVar as TypeVar +import Unison.Typechecker.Components (minimize') import Unison.Var (Var) import qualified Unison.Var as Var -- uncomment for debugging @@ -67,10 +68,10 @@ data Element v instance Var v => Show (Element v) where show (Var v) = case v of - TypeVar.Universal v -> Text.unpack (Var.shortName v) - TypeVar.Existential v -> "'"++Text.unpack (Var.shortName v) + TypeVar.Universal x -> "@" <> show x + TypeVar.Existential x -> "'" ++ show x show (Solved v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t - show (Ann v t) = Text.unpack (Var.shortName v)++" : "++show t + show (Ann v t) = Text.unpack (Var.shortName v) ++ " : " ++ show t show (Marker v) = "|"++Text.unpack (Var.shortName v)++"|" (===) :: Eq v => Element v -> Element v -> Bool @@ -546,7 +547,9 @@ instantiateR t v = getContext >>= \ctx -> case Type.monotype t >>= solve ctx v o setContext $ ctx `append` context [Marker x', Existential x'] instantiateR (ABT.bind body (Type.existential x')) v modifyContext (retract (Marker x')) - _ -> fail $ "could not instantiate right " ++ show t + _ -> do + logContext ("failed: instantiateR " <> show t <> " " <> show v) + fail $ "could not instantiate right " ++ show t withEffects :: [Type v] -> M v a -> M v a withEffects abilities' m = @@ -593,7 +596,7 @@ check e t = getContext >>= \ctx -> scope ("check: " ++ show e ++ ": " ++ show a <- synthesize e; ctx <- getContext subtype (apply ctx a) (apply ctx t) (as, t') = Type.stripEffect t - in withEffects as $ go e t' + in withEffects as $ go (minimize' e) t' else scope ("context: " ++ show ctx) . scope ("term: " ++ show e) . @@ -618,6 +621,7 @@ annotateLetRecBindings letrec = do -- annotate each term variable w/ corresponding existential -- [marker e1, 'e1, 'e2, ... v1 : 'e1, v2 : 'e2 ...] appendContext $ context (Marker e1 : map Existential es ++ zipWith Ann vs (map Type.existential es)) + logContext "annotating letrec bindings" -- check each `bi` against `ei`; sequencing resulting contexts Foldable.traverse_ (\(e,(_,binding)) -> check binding (Type.existential e)) (zip es bindings) -- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`; @@ -632,7 +636,8 @@ annotateLetRecBindings letrec = do -- | Synthesize the type of the given term, updating the context in the process. -- | Figure 11 from the paper synthesize :: Var v => Term v -> M v (Type v) -synthesize e = scope ("synth: " ++ show e) $ logContext "synthesize" >> go e where +synthesize e = scope ("synth: " ++ show e) $ go (minimize' e) + where go :: Var v => Term v -> M v (Type v) go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var Nothing -> fail $ "type not known for term var: " ++ Text.unpack (Var.name v) @@ -838,7 +843,7 @@ synthesizeApp ft arg = scope ("synthesizeApp: " ++ show ft ++ " " ++ show arg) $ ambientEs <- getAbilities o <$ check arg (Type.effect ambientEs i) go (Type.Existential' a) = do -- a^App - [i,o] <- traverse freshenVar [a, ABT.v' "o"] + [i,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"] let soln = Type.Monotype (Type.existential i `Type.arrow` Type.existential o) let ctxMid = context [Existential o, Existential i, Solved a soln] modifyContext' $ replace (Existential a) ctxMid diff --git a/parser-typechecker/src/Unison/Var.hs b/parser-typechecker/src/Unison/Var.hs index e83326266..024573987 100644 --- a/parser-typechecker/src/Unison/Var.hs +++ b/parser-typechecker/src/Unison/Var.hs @@ -24,7 +24,7 @@ import qualified Data.Set as Set -- info attached to `v` values may participate in the `Eq` or `Ord` instances, -- it is 'just' metadata. -- -class (Eq v, Ord v) => Var v where +class (Show v, Eq v, Ord v) => Var v where named :: Text -> v rename :: Text -> v -> v name :: v -> Text diff --git a/parser-typechecker/tests/Unison/Test/Typechecker.hs b/parser-typechecker/tests/Unison/Test/Typechecker.hs index 669ebe7cd..36c2bb71c 100644 --- a/parser-typechecker/tests/Unison/Test/Typechecker.hs +++ b/parser-typechecker/tests/Unison/Test/Typechecker.hs @@ -125,6 +125,17 @@ test = scope "typechecker" . tests $ |r12 : UInt64 |r12 = (x -> x) 64 | + |id : forall a . a -> a + |id x = x + | + |r13 : (UInt64, Text) + |r13 = let + | id = ((x -> x): forall a . a -> a) + | (id 10, id "foo") + | + |r14 : (forall a . a -> a) -> (UInt64, Text) + |r14 id = (id 10, id "foo") + | |() |] , checks [r|effect Abort where @@ -156,7 +167,19 @@ test = scope "typechecker" . tests $ |bork = u -> 1 +_UInt64 (Abort.Abort ()) | |() |] - , checks [r|--State effect + , checks [r|--State1 effect + |effect State se2 where + | put : ∀ se . se -> {State se} () + | get : ∀ se . () -> {State se} se + | + |state woot eff = case eff of + | { State.get () -> k } -> handle state woot in k woot + | { State.put snew -> k } -> handle (state snew) in (k ()) + | { a } -> (woot, a) + | + |() + |] + , checks [r|--State2 effect |effect State se2 where | put : ∀ se . se -> {State se} () | get : ∀ se . () -> {State se} se @@ -165,13 +188,13 @@ test = scope "typechecker" . tests $ |state woot eff = case eff of | { State.get () -> k } -> handle (state woot) in (k woot) | { State.put snew -> k } -> handle (state snew) in (k ()) - | { a } -> (woot, a) | - |ex : (UInt64, UInt64) - |ex = handle (state 42) in State.get () - | - |ex + |() |] + + --ex : (UInt64, UInt64) + --ex = handle (state 42) in State.get () + ] where c tm typ = scope tm . expect $ check (stripMargin tm) typ bombs s = scope s (expect . not . fileTypechecks $ s)