search

IaFP / ghc

A slightly more Glorious Haskell Compiler
Other
2 stars 0 forks source link

Pattern matching on data constructors with Rank N functions #42

Open fxdpntthm opened 2 years ago

fxdpntthm commented 2 years ago 
newtype NT m a = MkNT {unNT :: forall b. a -> m b}

foobar1 :: (b -> a) -> NT m a -> NT m b
foobar1 f nt = MkNT $ \ a -> unNT nt (f a)

foobar2 :: (b -> a) -> NT m a -> NT m b
foobar2 f (MkNT nt) = MkNT $ \ a -> nt (f a)

Although they both should work, foobar1 doesn't. The use of unNT gives rise to a wanted m @ b constraint. one could type foobar1 :: Total m => (b -> a) -> NT m a -> NT m b. The total constraint is needed here as m as it can be applied to any b