diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-12-18 11:29:13 -0500 |
| commit | 4eb93836d04d18f43d8c4360f290a7977d96c468 (patch) | |
| tree | ef38476a5b0199272d5dc20a65a306b4c7b2a112 /src/elab.sml | |
| parent | 37cf82d0761088c469205b90e35569674707202f (diff) | |
Add a new scoping check for unification variables, to fix a type inference bug
Diffstat (limited to 'src/elab.sml')
| -rw-r--r-- | src/elab.sml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/elab.sml b/src/elab.sml index c042d916..15365951 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2011, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -38,12 +38,16 @@ datatype kind' = | KTuple of kind list | KError - | KUnif of ErrorMsg.span * string * kind option ref - | KTupleUnif of ErrorMsg.span * (int * kind) list * kind option ref + | KUnif of ErrorMsg.span * string * kunif ref + | KTupleUnif of ErrorMsg.span * (int * kind) list * kunif ref | KRel of int | KFun of string * kind +and kunif = + KUnknown of kind -> bool (* Is the kind a valid unification? *) + | KKnown of kind + withtype kind = kind' located datatype explicitness = @@ -78,7 +82,11 @@ datatype con' = | CProj of con * int | CError - | CUnif of int * ErrorMsg.span * kind * string * con option ref + | CUnif of int * ErrorMsg.span * kind * string * cunif ref + +and cunif = + Unknown of con -> bool (* Is the constructor a valid unification? *) + | Known of con withtype con = con' located |