Changes between Version 38 and Version 39 of Holes

Timestamp:

05/17/12 01:00:52 (12 months ago)

Author:

simonpj

Comment:

--

Holes

@@ -141 +141 @@
 Note that all type variables should be the same for all reports, so all types above refer to the same `m`. 
 
+'''SLPJ''' see comments below about class constraints on the holes. '''End of SLPJ'''
+
+
 === Expressions ===
 
@@ -159 +162 @@
 Inferred type: MonadPlus m => m b
 }}}
-Again, note that the type variables are universally quantified over all reports, not each report separately.
+Again, note that the type variables are universally quantified over all reports, not each report separately.  '''SLPJ''' I have no idea what this sentence means.  '''End of SLPJ'''.
+
+'''SLPJ'''.  I am very uncomfortable with saying anything like
+{{{
+Inferred type: MonadPlus m => m b
+}}}
+for two reasons:
+ * First, that absolutely is not the inferred type of the hold.  Imagine that I added a binding
+{{{
+boo :: MonadPlus m => m b
+}}}
+ and replaced the last line of the example with
+{{{
+  y `mplus` boo
+}}}
+ Would it type check?  Absolutely not!  Adding type constraints on the types of the holes seems wierd and and impossible to justify.
+
+ * Second, the need for `MonadPlus` is nothing to do with the holes. It's to do with the call to `mplus` and the do-notation. It seems wrong to implicate the hole.
+'''End of SLPJ'''
+
 
 === Comparison ===
@@ -253 +275 @@
 If we instead allow the program to type-check, we can find out what type the hole should have ({{{_?h :: Show a => a}}} in this case) and more information.
 
+'''SLPJ''' I would rather put it like this. If I wrote
+{{{
+f :: String
+f = show undefined
+}}}
+then I '''want''' an ambiguity error.  And that is supposed to be what holes are equivalent to (see above).  But, you may argue, there is no point in reporting a cascade of errors that follow from the absence of information about a hole.  It's just distracting.  So here's an idea:
+ * With `-XHoles` we autmatically behave like `-fdefer-type-errors` for any unsolved type constraint that shares a free unification variable with a hole.
+The idea is that if we have a hole of type `a`, then an unsolved `(Show a)` or `(C [a])` or `F a ~ Int` or anything mentioning `a` are automatically deferred and perhaps not even reported as warnings (unsure on this point). If you run the program you might trip over one of them, of course.
+'''End of SLPJ'''
+
 A hole with an ambiguous type should probably be treated as a hole runtime error and not a deferred type error (see [#Runtimeerror Runtime error] for an example); however, not all holes are the immediate cause of ambiguity type errors. For example, consider:
 {{{