Newest at the top
| 2025-12-11 17:23:21 +0100 | <tomsmeding> | GHC makes some arbitrary rewriting choice when handling the equality `a ~ ?hole` introduced by the + |
| 2025-12-11 17:23:17 +0100 | <haskellbridge> | <matti palli> the type of the home becomes a, not the other way around |
| 2025-12-11 17:22:57 +0100 | <tomsmeding> | kuribas: or you have (Read a, Num a) => a, with the hole also of type a |
| 2025-12-11 17:22:37 +0100 | <kuribas> | tomsmeding: (read undefined :: Read a => a), after + it becomes (Read a, Num a), and (_ :: ?hole1), so after unifying with the hole, you have (Read ?hole, Num ?hole) => ?hole |
| 2025-12-11 17:22:28 +0100 | <tomsmeding> | and also that feels like fragile code, especially in GHC where you have zonking |
| 2025-12-11 17:22:16 +0100 | <tomsmeding> | but I'm not sure that characterises precisely what kuribas intends |
| 2025-12-11 17:21:59 +0100 | <tomsmeding> | you can try to deduce that fixing the type of the whole would resolve the ambiguity, perhaps |
| 2025-12-11 17:21:30 +0100 | <haskellbridge> | <matti palli> but yeah you are completely right, the ambiguity isn’t introduced by the hole, it’s just that the hole isn’t resolving any ambiguity (nor should it!) |
| 2025-12-11 17:20:47 +0100 | <tomsmeding> | but kuribas what do you think about my little example? |
| 2025-12-11 17:20:34 +0100 | <haskellbridge> | <matti palli> well yes but it shouldn’t escape the scope (you’d get the skolem has escaped warning haha) |
| 2025-12-11 17:20:01 +0100 | <tomsmeding> | well, if the type of the hole starts off as a type variable, that variable was completely new, wasn't it? ;) |
| 2025-12-11 17:19:29 +0100 | <haskellbridge> | <matti palli> it never comes up with a completely new variable |
| 2025-12-11 17:19:16 +0100 | <tomsmeding> | right |
| 2025-12-11 17:19:10 +0100 | <haskellbridge> | <matti palli> tomsmeding: technically the type of the hole starts of as a type variable, but is then quickly unified with variables that exist in scope. |
| 2025-12-11 17:19:08 +0100 | <tomsmeding> | how would GHC decide? |
| 2025-12-11 17:19:04 +0100 | <tomsmeding> | what if you have `read undefined + _`; that has an ambiguous type, but is that type "given rise to" by the hole? |
| 2025-12-11 17:18:31 +0100 | <tomsmeding> | if the type of the hole itself is the ambiguous type variable, then sure, it clearly "gives rise" to it (though even then, there's not at all necessarily a causal relationship!) |
| 2025-12-11 17:17:44 +0100 | <tomsmeding> | you can track dependencies of everything, but that likely slows down type checking significantly |
| 2025-12-11 17:17:30 +0100 | <tomsmeding> | every term gives rise to potentially multiple unification variables, and a lot of those are equal |
| 2025-12-11 17:17:12 +0100 | <tomsmeding> | "the hole gives rise to a type variable" is not a thing |
| 2025-12-11 17:17:07 +0100 | <haskellbridge> | <matti palli> You could get there by just giving a more specific type to the hole "_ :: blah", resolving the ambiguity |
| 2025-12-11 17:16:59 +0100 | <kuribas> | tomsmeding: the hole gives rise to a type variable, which can be either unified with something, or remains "ambiguous". In the latter case you can trace which type classes depend on the ambiguous variable, no? |
| 2025-12-11 17:16:13 +0100 | <tomsmeding> | but that would be -fdefer-type-errors behaviour, not -fdefer-typed-holes |
| 2025-12-11 17:16:03 +0100 | <tomsmeding> | one thing that's probably implementable (I say without having ever looked at the GHC typechecker) is instantiating any ambiguous unification variable with a special type such that unsolved constraints that mention that special type get magically solved with an error |
| 2025-12-11 17:14:23 +0100 | <tomsmeding> | also, the graph needs to include type variables |
| 2025-12-11 17:14:16 +0100 | <tomsmeding> | perhaps, but I expect you're going to have a lot of spurious dependencies |
| 2025-12-11 17:13:54 +0100 | <kuribas> | tomsmeding: isn't that use a graph on the typeclass dependencies? |
| 2025-12-11 17:13:43 +0100 | <tomsmeding> | and replacing arbitrary unsolved constraints with errors (and thus not stopping compilation for them) is rather against the idea of -fdefer-typed-holes |
| 2025-12-11 17:13:22 +0100 | <tomsmeding> | it's just hard to draw the line between an arbitrary unsolved constraint and one that is "intuitively" part of the hole |
| 2025-12-11 17:12:56 +0100 | <tomsmeding> | because instantiating a typeclass dictionary argument with an error term is very much expressible in Core, at least |
| 2025-12-11 17:12:43 +0100 | <kuribas> | yeah |
| 2025-12-11 17:12:31 +0100 | <tomsmeding> | is the problem here that you want to be sure that the unsolvable constraint is _purely_ due to a typed hole? |
| 2025-12-11 17:12:12 +0100 | <haskellbridge> | <matti palli> sure, you can do that with undefined or error as well. but then you have the issue of ambiguous type variables, as you’ve encountered |
| 2025-12-11 17:11:17 +0100 | <kuribas> | That's how large proofs are done, you treat some parts as "assumptions", and proof them later. Or they turn out to be false, and you have to abort the whole proof (or find another proof). |
| 2025-12-11 17:10:58 +0100 | <haskellbridge> | <matti palli> what I mean is that you solve the constraint and emit a witness that is the dictionary |
| 2025-12-11 17:10:15 +0100 | <haskellbridge> | <matti palli> yeah sure, you can emit a “proof” that just contains error |
| 2025-12-11 17:10:15 +0100 | <lucabtz> | i remember a video of tsoding on youtube referring to implementing instances like the functor instance as "proving" something is a functor |
| 2025-12-11 17:10:15 +0100 | <kuribas> | Then they are just "assumptions". |
| 2025-12-11 17:10:09 +0100 | <kuribas> | Even so, proof assistants like agda and idris allow you to have holes as proofs. |
| 2025-12-11 17:09:33 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2025-12-11 17:08:36 +0100 | <kuribas> | Due to bottom. |
| 2025-12-11 17:08:30 +0100 | <kuribas> | haskell doesn't really have "proofs". |
| 2025-12-11 17:07:39 +0100 | <haskellbridge> | <matti palli> and it’s simultaneously the dictionary which contains the code, afaiu |
| 2025-12-11 17:06:46 +0100 | <haskellbridge> | <matti palli> yeah, and the right instance is the proof |
| 2025-12-11 17:06:05 +0100 | <kuribas> | You don't emit a "proof", the type inference does a proof search to find the right instance. |
| 2025-12-11 17:05:30 +0100 | <haskellbridge> | <matti palli> that’s how the typechecker works, you solve constraint by emitting a “proof” that the constraint holds, and that contains the dictionary which contains the code |
| 2025-12-11 17:05:30 +0100 | yin | (~zero@user/zero) zero |
| 2025-12-11 17:05:26 +0100 | <kuribas> | And the point is that the hole is not just "an error", but allows you to fill in the rest of the program, while leave out details. |
| 2025-12-11 17:05:15 +0100 | yin | (~zero@user/zero) (Remote host closed the connection) |
| 2025-12-11 17:04:40 +0100 | <kuribas> | constraints are just implicits. |