Type applications in patterns should also work for universal type variables
Consider
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
module Lib where
import Data.Void
data SMaybe a
= SNothing
| SJust !a
deriving Read
foo :: Read a => (SMaybe a -> r) -> String -> r
foo f s = f (read s)
bar :: _
bar = foo (\(SNothing @Void) -> 42 :: Int) "SNothing"
This compiles and infers bar :: Int
on HEAD. Nice!
But it doesn't seem to work in the presence of a type index:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Lib where
data SBool (b :: Bool) where
STrue :: forall b. (b ~ 'True) => SBool b
SFalse :: forall b. (b ~ 'False) => SBool b
class Blah b where
blah :: SBool b
instance Blah 'True where
blah = STrue
foo :: Blah b => (SBool b -> Int) -> Int
foo f = f blah
bar = foo (\(STrue @True) -> 42)
Error:
test.hs:24:7: error:
• Ambiguous type variable ‘b0’ arising from a use of ‘foo’
prevents the constraint ‘(Blah b0)’ from being solved.
Probable fix: use a type annotation to specify what ‘b0’ should be.
These potential instance exist:
instance Blah 'True -- Defined at test.hs:18:10
• In the expression: foo (\ (STrue @True) -> 42)
In an equation for ‘bar’: bar = foo (\ (STrue @True) -> 42)
|
24 | bar = foo (\(STrue @True) -> 42)
| ^^^
Here, I expect the specification of @True
in the STrue
pattern to refine the universal type variable b
of the SBool
constructor, so that the type of the match is inferred to be SBool 'True
. This means I have to write STrue :: SBool 'True
.
I believe what happens is that the type variable b
of STrue
counts as an existential type variable. What a shame. I had hoped that https://dl.acm.org/doi/pdf/10.1145/3242744.3242753 somehow got rid of this distinction.
I feel like I want a bidirectional flow of information (@True
informing the match type, the provided constraints of STrue
informing any type variables in the match), like unification, instead of just matching the existentially bound var b
against the type application in the pattern True
and check whether that constraint (b ~ True
) is satisfiable.
This was all inspired by https://mail.haskell.org/pipermail/ghc-devs/2021-March/019703.html.