2025/03/21

Newest at the top

2025-03-21 16:25:56 +0100jackdk(sid373013@cssa/jackdk) jackdk
2025-03-21 16:25:08 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 16:24:44 +0100 <tomsmeding> that
2025-03-21 16:24:37 +0100 <tomsmeding> absence: Note that `Subset (x : list1) (x : list2)` is NOT equivalent to `Subset list1 list2`: the former allows elements of list1 to be equal to x, whereas the latter only allows that if x is in list2
2025-03-21 16:24:29 +0100 <int-e> Looks like Subset (x : list1) (x : list2) should simplify to Subset list1 (x : list2), but there's nothing that ensures that list1 doesn't contain another x...
2025-03-21 16:23:43 +0100aristid(sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 268 seconds)
2025-03-21 16:23:42 +0100jackdk(sid373013@cssa/jackdk) (Ping timeout: 244 seconds)
2025-03-21 16:23:29 +0100 <absence> Speaking of vibes, it feels vaguely similar to "(Monad (t m), Monad m, MonadTrans t) =>", so maybe something something QuantifiedConstraints...?
2025-03-21 16:22:57 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com) taktoa[c]
2025-03-21 16:22:45 +0100 <tomsmeding> ah, so `Subset list1 list2 => Subset (x : list1) (x : list2)` itself isn't even directly derivable
2025-03-21 16:21:38 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 244 seconds)
2025-03-21 16:21:17 +0100 <absence> Here's the constraint by the way: https://hackage.haskell.org/package/effectful-core-2.5.1.0/docs/src/Effectful.Internal.Effect.html…
2025-03-21 16:20:54 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 16:20:50 +0100 <tomsmeding> I'm not 100% sure this is what you are running into, but it has a similar "vibe" :p
2025-03-21 16:20:33 +0100 <tomsmeding> you have to modify the class
2025-03-21 16:20:29 +0100 <tomsmeding> no
2025-03-21 16:20:11 +0100 <absence> Can I do that if the constraint and the function that needs it are defined in a third-party library?
2025-03-21 16:19:58 +0100 <tomsmeding> if you don't know what I'm talking about, or don't know how it applies to your case, you'll have to share the definition of that Subset thing
2025-03-21 16:19:35 +0100 <tomsmeding> the latter is normally _not_ what GHC does
2025-03-21 16:19:26 +0100 <tomsmeding> that allows ghc to, given an `instance C A => C T` not only infer `C T` from `C A`, but furthermore conclude from evidence of `C T` that `C A` must also hold
2025-03-21 16:18:44 +0100 <tomsmeding> absence: I have a feeling that this is an X-Y problem, and that the answer is a common-ish trick that I don't know a name for: define an associated type family to your class where the right-hand sides are precisely the instance contexts, then add that type family as a _superclass_ constraint to the class
2025-03-21 16:17:53 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 16:16:55 +0100 <absence> When using a constraint called Subset, which takes two type-level lists, I find myself having to use "Subset (x : list1) (x : list2) => ..." instead of just "Subset list1 list2". Is there a way to convince the type checker that the x is superfluous?
2025-03-21 16:16:48 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2025-03-21 16:15:31 +0100bsima(~bsima@143.198.118.179) bsima
2025-03-21 16:15:06 +0100bsima(~bsima@143.198.118.179) (Quit: ZNC 1.8.2 - https://znc.in)
2025-03-21 16:14:20 +0100berzerk(~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 16:12:25 +0100as___(~as@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 16:11:49 +0100as__(~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 244 seconds)
2025-03-21 16:08:17 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 16:07:58 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 16:07:07 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 16:06:48 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-03-21 16:02:24 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 16:02:16 +0100notdabs(~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4)
2025-03-21 16:02:14 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-03-21 15:59:19 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 15:59:01 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 15:58:04 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-03-21 15:57:03 +0100ft(~ft@p508db463.dip0.t-ipconnect.de) ft
2025-03-21 15:54:42 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 15:52:53 +0100euleritian(~euleritia@95.90.214.149) (Read error: Connection reset by peer)
2025-03-21 15:51:04 +0100SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder
2025-03-21 15:50:06 +0100as__(~as@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 15:49:51 +0100kh0d(~kh0d@109.111.226.14) kh0d
2025-03-21 15:49:15 +0100Buliarou1(~gypsydang@46.232.210.139) Buliarous
2025-03-21 15:49:02 +0100myme(~myme@2a01:799:d5e:5f00:69c6:1b0c:ff6d:bdea) myme
2025-03-21 15:46:35 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) jespada
2025-03-21 15:40:29 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 15:38:17 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…)