shithub: MicroHs

--- a/TODO

+++ b/TODO

@@ -23,3 +23,5 @@

   - allow generalization for local bindings

   - use subsumption (like if) in the arms of alternatives.

   - allow missing top level signatures (and generalize)

+  - instead of skolemization, use regular variables, making sure they are unique

\ No newline at end of file

--- a/src/MicroHs/TypeCheck.hs

+++ b/src/MicroHs/TypeCheck.hs

@@ -509,10 +509,11 @@

         EApp fb xb -> T.do { unify loc fa fb; unify loc xa xb }

         EUVar i    -> addUVar i a

         _          ->

-          --trace ("impossible unify " ++ showExpr a ++ " = " ++ showExpr b) $

+          --Xtrace ("impossible unify 1 " ++ showExpr a ++ " = " ++ showExpr b) $

           impossible

     EUVar i -> addUVar i b

-    _ -> impossible

+    _ -> --Xtrace ("impossible unify 2 " ++ showExpr a ++ " = " ++ showExpr b) $

+         impossible

{-

 unMType :: Expected -> T EType

@@ -903,7 +904,15 @@

           -- Type checking an expression (or type)

           T.when (isUnderscore i) impossible

           (e, t) <- tLookup "variable" i

-          instSigma loc t mt

+          -- Variables bound in patterns start with an (EUVar ref) type,

+          -- which can be instantiated to a polytype.

+          -- Dereference such a ref.

+          t' <-

+            case t of

+              EUVar r -> T.fmap (fromMaybe t) (getUVar r)

+              _ -> T.return t

+--          traceM ("EVar " ++ showIdent i ++ " :: " ++ showExpr t ++ " = " ++ showExpr t')

+          instSigma loc t' mt

           T.return e

     EApp f a -> T.do

@@ -1086,8 +1095,9 @@

   ites <- T.mapM (opfix fixs) aies

   T.return $ calc [ae] [] ites

-unArrow :: SLoc -> EType -> T (EType, EType)

-unArrow loc t =

+unArrow :: --XHasCallStack =>

+           SLoc -> EType -> T (EType, EType)

+unArrow loc t = T.do

   case getArrow t of

     Just ar -> T.return ar

     Nothing -> T.do

--- a/tests/Rank2.hs

+++ b/tests/Rank2.hs

@@ -17,4 +17,4 @@

   putStrLn $ showPair showInt showBool $ f id

   putStrLn $ showPair showInt showBool $ g const

   case iD of

-    Id i -> showPair showInt showBool (i 1, i True)

+    Id i -> putStrLn $ showPair showInt showBool (i 1, i True)

--- a/tests/Rank2.ref

+++ b/tests/Rank2.ref

@@ -1,2 +1,3 @@

 (1,True)

 (1,True)

+(1,True)

--

⑨