summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml14
1 files changed, 13 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f0aa8d7a..6b25cedb 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -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