Newest at the top
2024-05-14 23:45:16 +0200 | Sgeo | (~Sgeo@user/sgeo) |
2024-05-14 23:36:38 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) |
2024-05-14 23:35:41 +0200 | kadir | (~kadir@85.103.183.96) (Quit: WeeChat 4.2.2) |
2024-05-14 23:34:23 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2024-05-14 23:26:01 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
2024-05-14 23:25:25 +0200 | esnos | (~user@194.29.137.22) (Remote host closed the connection) |
2024-05-14 23:23:27 +0200 | causal | (~eric@50.35.88.207) |
2024-05-14 23:22:04 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds) |
2024-05-14 23:18:32 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2024-05-14 23:17:12 +0200 | euphores | (~SASL_euph@user/euphores) |
2024-05-14 23:14:42 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2024-05-14 23:11:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-05-14 23:11:23 +0200 | ph88 | (~ph88@2a02:8109:9e26:c800:50c2:30a5:77d8:a72f) (Remote host closed the connection) |
2024-05-14 23:08:37 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
2024-05-14 23:07:04 +0200 | yin | (~yin@user/zero) |
2024-05-14 23:06:07 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 260 seconds) |
2024-05-14 23:05:19 +0200 | Moyst | (~moyst@user/moyst) |
2024-05-14 23:03:53 +0200 | Moyst | (~moyst@user/moyst) (Ping timeout: 272 seconds) |
2024-05-14 23:00:05 +0200 | yin | (~yin@user/zero) (Ping timeout: 240 seconds) |
2024-05-14 22:52:16 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
2024-05-14 22:36:05 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 240 seconds) |
2024-05-14 22:35:06 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
2024-05-14 22:34:53 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 240 seconds) |
2024-05-14 22:34:09 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
2024-05-14 22:29:13 +0200 | greenflower | (~greenflow@103.191.25.63) (Quit: Client closed) |
2024-05-14 22:23:04 +0200 | cayley5 | (~cayley5@user/phileasfogg) |
2024-05-14 22:22:42 +0200 | cayley5 | (~cayley5@user/phileasfogg) (Quit: Ping timeout (120 seconds)) |
2024-05-14 22:22:10 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
2024-05-14 22:08:39 +0200 | <tomsmeding> | raehik: notable is that :t'ing that doesn't work, you actually have to try to show the Proxy |
2024-05-14 22:07:53 +0200 | <raehik> | tomsmeding: oh nice catch. I had managed to write a similar definition that somehow did not evaluate the type, so was thinking I needed something more in depth |
2024-05-14 22:06:13 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection) |
2024-05-14 22:04:00 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) |
2024-05-14 22:01:46 +0200 | <tomsmeding> | but to get it to show it has to typecheck, hence you have to evaluate the type |
2024-05-14 22:01:36 +0200 | <tomsmeding> | using Proxy means that 1. the type can be whatever, and 2. it will always show if the type evaluates to something sensible |
2024-05-14 22:00:15 +0200 | <tomsmeding> | raehik: perhaps this works? |
2024-05-14 22:00:07 +0200 | <yahb2> | <interactive>:21:1: error: ; • test ; • When checking the inferred type ; it :: forall {k}. Proxy (TypeError ...) |
2024-05-14 22:00:07 +0200 | <tomsmeding> | % Proxy @(Id (TypeError (Text "test"))) |
2024-05-14 22:00:05 +0200 | <yahb2> | <no output> |
2024-05-14 22:00:05 +0200 | <tomsmeding> | % import Data.Proxy |
2024-05-14 22:00:02 +0200 | <yahb2> | <interactive>:17:1: error: Data constructor not in scope: Proxy |
2024-05-14 22:00:01 +0200 | <tomsmeding> | % Proxy @(Id (TypeError (Text "test"))) |
2024-05-14 21:59:53 +0200 | <yahb2> | <no output> |
2024-05-14 21:59:53 +0200 | <tomsmeding> | % :set -XTypeApplications |
2024-05-14 21:58:56 +0200 | <raehik> | thx for the help my docs will benefit from knowing this! |
2024-05-14 21:58:19 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
2024-05-14 21:57:31 +0200 | <tomsmeding> | -y |
2024-05-14 21:57:28 +0200 | <tomsmeding> | unfortunatelt |
2024-05-14 21:57:25 +0200 | <tomsmeding> | yeah I've always found :k! to be a bit unstable |
2024-05-14 21:57:16 +0200 | <tomsmeding> | ah :) |
2024-05-14 21:57:11 +0200 | <raehik> | tomsmeding: oh yep that works on 9.2. but my non-contrived example (that goes thru lots of type families) doesn't xd |