data Foo a where
Bar :: Foo [a]
foo :: Foo a -> ()
foo Bar = <body> -- we know (a ~ [b]) here, for some b
The pattern match on Bar in foo gives us the equality assumption on the right hand side, but
we don't have an easy way of capturing 'b' - which we might want to do for, say, visible type application inside <body>.
foo' :: Foo a -> ()
foo' (Bar :: Foo a) = <body>
of course works, but it only gives us access to 'a' in <body>.
foo'' :: Foo a -> ()
foo'' (Bar :: Foo [c]) = <body>
This would mean that in addition to (a ~ [b]), for some b, we would get (a ~ [c]), for our new c. This then gives (b ~ c),
essentially giving us access to the existential b. Of course we would need to check that our scoped type signature
doesn't introduce bogus coercions, like
foo''' :: Foo a -> ()
foo''' (Bar :: Foo [[c]]) = <body>
is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]), which we can't prove from the given assumptions.
_______________________________________________On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif <ggreif@gmail.com> wrote:
My original question, though, is not answered yet, namely why not to
detect that we are about to pattern match on a GADT constructor and
allow the programmer to capture the *refined* type with her type
annotation. Sure this would necessitate a change to the type checker,
but would also increase the expressive power a bit.
Is there some fundamental problem with this? Or simply nobody wanted
to do this yet? Would it be hard to implement type checking *after*
refinement on GADT(-like) patterns?I wouldn't be surprised if type checking is precisely what enables refinement, making this a bit chicken-and-egg.--
brandon s allbery kf8nh sine nomine associatesunix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs