Newest at the top
| 2025-12-11 18:02:14 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-12-11 17:53:17 +0100 | Guest87 | (~Guest87@2405:201:d006:986f:5c73:3a20:69d:7d07) |
| 2025-12-11 17:49:55 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 2025-12-11 17:46:40 +0100 | zero | yin |
| 2025-12-11 17:46:36 +0100 | yin | zero |
| 2025-12-11 17:45:17 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-12-11 17:45:02 +0100 | <dolio> | Even if you know the provenance of type variables, I don't know that the further idea makes sense. |
| 2025-12-11 17:43:45 +0100 | tv | (~tv@user/tv) (Read error: Connection reset by peer) |
| 2025-12-11 17:42:20 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 244 seconds) |
| 2025-12-11 17:41:38 +0100 | <haskellbridge> | interesting problem for sure |
| 2025-12-11 17:41:35 +0100 | <haskellbridge> | <matti palli> Right. At the moment there is no distinction, and thinking about it might be that typechecking levels could be an issue, i.e. when do you unify with a hole type variable in the new schema |
| 2025-12-11 17:41:16 +0100 | spew_ | spew |
| 2025-12-11 17:41:15 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 2025-12-11 17:40:43 +0100 | spew | (~spew@user/spew) (Ping timeout: 255 seconds) |
| 2025-12-11 17:40:12 +0100 | spew_ | (~spew@user/spew) spew |
| 2025-12-11 17:35:22 +0100 | bggd_ | (~bgg@2a01:e0a:fd5:f510:fb9e:194f:f1d5:eb88) (Remote host closed the connection) |
| 2025-12-11 17:32:47 +0100 | <kuribas> | Yes "fromJust :: Maybe a -> a", then "?hole ~ Maybe ?sub_hole", and "Show ?sub_hole" is deferred. |
| 2025-12-11 17:32:30 +0100 | spew | (~spew@user/spew) spew |
| 2025-12-11 17:32:06 +0100 | <haskellbridge> | SPJ bugged me about this, saying we should add provenance to type variables for improved errors. If you had that you could improve holes as well |
| 2025-12-11 17:32:06 +0100 | <haskellbridge> | <matti palli> tomsmeding: hmm yes interesting |
| 2025-12-11 17:31:46 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-12-11 17:30:58 +0100 | lucabtz | (~lucabtz@user/lucabtz) (Remote host closed the connection) |
| 2025-12-11 17:30:36 +0100 | <tomsmeding> | good luck :p |
| 2025-12-11 17:30:29 +0100 | <kuribas> | tomsmeding: right |
| 2025-12-11 17:30:28 +0100 | <tomsmeding> | ok I have to go, sorry |
| 2025-12-11 17:30:21 +0100 | <tomsmeding> | I think |
| 2025-12-11 17:30:19 +0100 | <tomsmeding> | matti: kuribas is arguing that a type variable "arising from" a hole originally should have a little tag saying so, and when unifying two type variables, you take the union of the tags |
| 2025-12-11 17:29:49 +0100 | <haskellbridge> | <matti palli> kuribas: but it doesn’t, it belongs to the undefined or the read |
| 2025-12-11 17:29:45 +0100 | <tomsmeding> | does the `a` in the `Maybe a` that is the type of `_`, arise from the hole? |
| 2025-12-11 17:29:30 +0100 | <tomsmeding> | what about `show (fromJust _)`? |
| 2025-12-11 17:29:18 +0100 | <kuribas> | tomsmeding: they are now, but like I said, I would tag it as belonging to a hole. |
| 2025-12-11 17:28:54 +0100 | <tomsmeding> | so they're rewritten in some direction, and one of the two disappears |
| 2025-12-11 17:28:43 +0100 | <tomsmeding> | but the unification variable resulting from `read ""` and the one resulting from `_` are the same to GHC |
| 2025-12-11 17:28:29 +0100 | <kuribas> | yes |
| 2025-12-11 17:28:01 +0100 | <tomsmeding> | and should `read "" + _` and `_ + read ""` have the same behaviour under -fdefer-typed-holes? |
| 2025-12-11 17:27:49 +0100 | <kuribas> | tomsmeding: I tag ?hole as a unification variable belonging to a hole, and any constraints on it are deferred as well. |
| 2025-12-11 17:27:38 +0100 | <tomsmeding> | right |
| 2025-12-11 17:27:28 +0100 | sindu | (~sindu@2.148.32.207.tmi.telenormobil.no) |
| 2025-12-11 17:27:22 +0100 | <kuribas> | tomsmeding: well it doesn't? |
| 2025-12-11 17:27:21 +0100 | <tomsmeding> | (I guess the 'undefined' is a red herring in all of this, `read ""` works just as well) |
| 2025-12-11 17:26:50 +0100 | <tomsmeding> | because if it doesn't, then -fdefer-typed-HOLES should not have an impact on GHC's behaviour when compiling `read undefined` |
| 2025-12-11 17:26:26 +0100 | <kuribas> | tomsmeding: why should it? |
| 2025-12-11 17:25:57 +0100 | <tomsmeding> | `read undefined` has no holes in haskell |
| 2025-12-11 17:25:49 +0100 | <kuribas> | tomsmeding: It'll happily generate an empty list of undefined type. |
| 2025-12-11 17:25:44 +0100 | <tomsmeding> | then it's -fdefer-type-errors, not -fdefer-typed-holes |
| 2025-12-11 17:25:35 +0100 | <kuribas> | tomsmeding: in idris it doesn't :) |
| 2025-12-11 17:25:32 +0100 | <tomsmeding> | if so, my `read undefined + _` makes it ambiguous whether it should throw an error or not |
| 2025-12-11 17:25:19 +0100 | <tomsmeding> | kuribas: if I write simply `read undefined` in a program without a hole, and I set -fdefer-typed-holes, should that result in an error? |
| 2025-12-11 17:24:54 +0100 | <tomsmeding> | because if it does depend on internal typechecker choices like these, then behaviour in practice will be highly unpredictable, which GHC in general considers worse than just not supporting the thing at all |
| 2025-12-11 17:24:28 +0100 | <kuribas> | tomsmeding: like you said, "read undefined" gives rise to a unification variable. |