Newest at the top
| 2024-11-18 16:00:14 +0100 | <dolio> | You could, but that's not the right type. |
| 2024-11-18 15:59:58 +0100 | <Wygulmage> | Right. Can I give it a type like `Int# -> (a ~ Bool)=> a` ? |
| 2024-11-18 15:59:24 +0100 | <dolio> | Okay, so, it only returns a Bool, not evidence that `a ~ Int`. |
| 2024-11-18 15:59:09 +0100 | <Wygulmage> | `unpack :: Int# -> Bool` |
| 2024-11-18 15:58:49 +0100 | <dolio> | It does in unpack. But what is the type of unpack ? |
| 2024-11-18 15:57:51 +0100 | <Wygulmage> | I assumed that strictly matching the GADT constructor Foo__ in the view pattern would bring the constraint into scope. |
| 2024-11-18 15:57:12 +0100 | <Wygulmage> | (actually `Int# -> Bool`, if that matters.) |
| 2024-11-18 15:57:10 +0100 | <dolio> | Oh I see. Anyway, it doesn't matter. It just swaps around the problem. |
| 2024-11-18 15:56:39 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 252 seconds) |
| 2024-11-18 15:55:56 +0100 | <dolio> | Right, but what type is `unpack`? |
| 2024-11-18 15:55:38 +0100 | <Wygulmage> | type of unpack is Int -> Bool |
| 2024-11-18 15:55:21 +0100 | <Wygulmage> | Sorry, so the GADT is `data Foo a where Foo__ :: Int -> Foo Bool |
| 2024-11-18 15:55:18 +0100 | lol_ | jcarpenter2 |
| 2024-11-18 15:54:12 +0100 | <dolio> | Like `data Witness c a where Wit :: c => a -> Witness c a` |
| 2024-11-18 15:53:14 +0100 | <dolio> | You need it to produce a type that is a Boolean with evidence that you're going to match on. |
| 2024-11-18 15:52:43 +0100 | <dolio> | Presumably the problem is that it just returns a boolean, which means that it doesn't actually get you the a ~ Int evidence that you say it has. |
| 2024-11-18 15:52:41 +0100 | Wygulmage | (~k`@user/Wygulmage) Wygulmage |
| 2024-11-18 15:52:41 +0100 | Wygulmage | (~k`@152.7.255.193) (Changing host) |
| 2024-11-18 15:50:16 +0100 | k` | Wygulmage |
| 2024-11-18 15:50:11 +0100 | <dolio> | What is the type of unpack? |
| 2024-11-18 15:49:41 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2024-11-18 15:44:15 +0100 | <k`> | The GHC docs seem to imply that that's how the second set of constraints works, but I can't get the type to check. |
| 2024-11-18 15:43:58 +0100 | euleritian | (~euleritia@176.2.4.196) |
| 2024-11-18 15:43:32 +0100 | euleritian | (~euleritia@77.22.252.159) (Ping timeout: 252 seconds) |
| 2024-11-18 15:41:56 +0100 | <k`> | Is it possible to include GADT constraints in a pattern synonym? I'm trying to do something like `pattern ()=> (a ~ Int)=> Bool -> Foo a ; pattern Foo b <- (unpack -> b) where Foo x = Foo__ (pack x)`, and I get type error "Couldn't match type 'a' with 'Bool'". |
| 2024-11-18 15:39:49 +0100 | willscripted | (~willscrip@user/willscripted) willscripted |
| 2024-11-18 15:38:18 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-11-18 15:37:24 +0100 | k` | (~k`@152.7.255.193) |
| 2024-11-18 15:22:12 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3113-e8b3-4dc5-4d20-737c-18a7.rev.sfr.net) alexherbo2 |
| 2024-11-18 15:11:21 +0100 | ystael | (~ystael@user/ystael) ystael |
| 2024-11-18 15:07:56 +0100 | euleritian | (~euleritia@77.22.252.159) |
| 2024-11-18 15:07:35 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-11-18 15:07:31 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-11-18 15:05:59 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) |
| 2024-11-18 15:05:08 +0100 | euleritian | (~euleritia@77.22.252.159) (Read error: Connection reset by peer) |
| 2024-11-18 15:01:31 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-11-18 15:01:05 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 265 seconds) |
| 2024-11-18 14:59:46 +0100 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-11-18 14:57:52 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-11-18 14:53:35 +0100 | astroanax | (~astroanax@2001:19f0:7402:f82:5400:1ff:fec4:f7d7) astroanax |
| 2024-11-18 14:52:43 +0100 | astroanax | (~astroanax@2001:19f0:7402:f82:5400:1ff:fec4:f7d7) (Ping timeout: 244 seconds) |
| 2024-11-18 14:48:45 +0100 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) manwithluck |
| 2024-11-18 14:48:20 +0100 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) (Remote host closed the connection) |
| 2024-11-18 14:42:43 +0100 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
| 2024-11-18 14:41:44 +0100 | euleritian | (~euleritia@77.22.252.159) |
| 2024-11-18 14:41:25 +0100 | euleritian | (~euleritia@dynamic-176-007-160-241.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-11-18 14:40:59 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2024-11-18 14:39:58 +0100 | euleritian | (~euleritia@dynamic-176-007-160-241.176.7.pool.telefonica.de) |
| 2024-11-18 14:33:00 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-11-18 14:31:55 +0100 | zlqrvx | (~zlqrvx@user/zlqrvx) (Ping timeout: 264 seconds) |