Mercurial > urweb

diff src/elaborate.sml @ 898:d1d0b18afd3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Working on Grid; have gone from one dynamic table bizareness to another
author Adam Chlipala <adamc@hcoop.net>
date Sun, 19 Jul 2009 17:45:02 -0400
parents e571fb150a9f
children 6d9538ce94d8
line wrap: on
line diff
--- a/src/elaborate.sml	Sat Jul 18 15:08:21 2009 -0400
+++ b/src/elaborate.sml	Sun Jul 19 17:45:02 2009 -0400
@@ -1116,6 +1116,18 @@
 
  fun elabHead (env, denv) infer (e as (_, loc)) t =
      let
+         fun unravelKind (t, e) =
+             case hnormCon env t of
+                 (L'.TKFun (x, t'), _) =>
+                 let
+                     val u = kunif loc
+
+                     val t'' = subKindInCon (0, u) t'
+                 in
+                     unravelKind (t'', (L'.EKApp (e, u), loc))
+                 end
+               | t => (e, t, [])
+
          fun unravel (t, e) =
              case hnormCon env t of
                  (L'.TKFun (x, t'), _) =>
@@ -1184,7 +1196,7 @@
                | t => (e, t, [])
      in
          case infer of
-             L.DontInfer => (e, t, [])
+             L.DontInfer => unravelKind (t, e)
            | _ => unravel (t, e)
      end