blob: 59248c9a056bf0b3d5259dcf122333a2afc2b896 (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
;;; File: type/unify.scm Author: John
;;; This is the basic unification algorithm used in type checking.
;;; Unification failure invokes the current type error handler
;;; Start by removing instantiated type variables from the type.
(define (unify type1 type2)
(unify-1 (prune type1) (prune type2)))
;;; The only real tweak here is the read-only bit on type variables.
;;; The rule is that a RO tyvar can be unified only with a generic
;;; non-RO tyvar which has the same or more general context.
;;; Aside from this, this is standard unification except that context
;;; propagation is needed when a tyvar with a non-empty context is
;;; instantiated.
;;; If type2 is a tyvar and type1 is not they are switched.
(define (unify-1 type1 type2)
(cond ((eq? type1 type2) ;; this catches variable to variable unify
'OK)
((ntyvar? type1)
(cond ((occurs-in-type type1 type2)
(type-error "Circular type: cannot unify ~A with ~A"
type1 type2))
((ntyvar-read-only? type1)
(cond ((or (not (ntyvar? type2)) (ntyvar-read-only? type2))
(type-error
"Signature too general: cannot unify ~A with ~A"
type1 type2))
(else
(unify-1 type2 type1))))
((and (ntyvar? type2)
(ntyvar-read-only? type2)
(non-generic? type1))
(type-error
"Type signature cannot be used: monomorphic type variables present."))
(else
(instantiate-tyvar type1 type2)
(let ((classes (ntyvar-context type1)))
(if (null? classes)
'OK
(propagate-contexts/ntype type1 type2 classes))))))
((ntyvar? type2)
(unify-1 type2 type1))
((eq? (ntycon-tycon type1) (ntycon-tycon type2))
(unify-list (ntycon-args type1) (ntycon-args type2)))
(else
(let ((etype1 (expand-ntype-synonym type1))
(etype2 (expand-ntype-synonym type2)))
(if (same-tycon? (ntycon-tycon etype1) (ntycon-tycon etype2))
(unify-list (ntycon-args etype1) (ntycon-args etype2))
;; This error message should probably show both the original
;; and the expanded types for clarity.
(type-error
"Type conflict: type ~A does not match ~A"
etype1 etype2))))))
(define-integrable (instantiate-tyvar tyvar val)
(setf (ntyvar-value tyvar) val))
;;; This is needed since interface files may leave multiple def's
;;; for the same tycon sitting around.
(define (same-tycon? ty1 ty2)
(or (eq? ty1 ty2)
(and (eq? (def-name ty1) (def-name ty2))
(eq? (def-module ty1) (def-module ty2)))))
;;; unifies two lists of types pairwise. Used for tycon args.
(define (unify-list args1 args2)
(if (null? args1)
'OK
(begin (unify-list (cdr args1) (cdr args2))
(unify (car args1) (car args2)))))
;;; combines a list of types into a single type. Used in constructs
;;; such as [x,y,z] and case expressions.
(define (unify-list/single-type types)
(when (not (null? types))
(let ((type (car types)))
(dolist (type2 (cdr types))
(unify type type2)))))
;;; This propagates the context from a just instantiated tyvar to the
;;; instantiated value. If the value is a tycon, instances must be
;;; looked up. If the value is a tyvar, the context is added to that of
;;; other tyvar.
;;; This is used to back out of the unification on errors. This is a
;;; poor mans trail stack! Without this, error messages get very
;;; obscure.
(define *instantiated-tyvar* '())
(define (propagate-contexts/ntype tyvar type classes)
(dynamic-let ((*instantiated-tyvar* tyvar))
(propagate-contexts/inner type classes)))
(define (propagate-contexts/inner type classes)
(let ((type (prune type)))
(if (ntyvar? type)
(if (ntyvar-read-only? type)
(if (context-implies? (ntyvar-context type) classes)
'OK ; no need for context propagation here
(begin
(setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f)
(type-error "Signature context is too general")))
(if (null? (ntyvar-context type))
(setf (ntyvar-context type) classes)
(setf (ntyvar-context type)
(merge-contexts classes (ntyvar-context type)))))
(propagate-contexts-1 (expand-ntype-synonym type) classes))))
;;; The type has now been expanded. This propagates each class constraint
;;; in turn.
(define (propagate-contexts-1 type classes)
(dolist (class classes)
(propagate-single-class type class)))
;;; Now we have a single class & data type. Either an instance decl can
;;; be found or a type error should be signalled. Once the instance
;;; decl is found, contexts are propagated to the component types.
(define (propagate-single-class type class)
(let ((instance (lookup-instance (ntycon-tycon type) class)))
(cond ((eq? instance '#f)
;; This remove the instantiation which caused the type
;; error - perhaps stop error propagation & make
;; error message better.
(setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f)
(type-error "Type ~A is not in class ~A" type class))
(else
;; The instance contains a list of class constraints for
;; each argument. This loop pairs the argument to the
;; type constructor with the context required by the instance
;; decl.
(dolist2 (classes (instance-gcontext instance))
(arg (ntycon-args type))
(propagate-contexts/inner arg classes)))))
'OK)
;;; The routines which handle contexts (merge-contexts and context-implies?)
;;; are in type-utils. The occurs check is also there.
|
