#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
Reporter: simonpj | Owner: simonpj
Type: bug | Status: new
Priority: high | Milestone: 7.0.1
Component: Compiler | Version: 6.12.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Comment(by pumpkin):
Oh! I see the difference now!
Matching on a GADT constructor introduces a type equality context on the
matched variables, but doesn't refine them explicitly, as far as I can
tell.
To test this, in addition to the
{{{
test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC
}}}
example above, I wrote the following:
{{{
test' :: (n ~ Nz) => Fin n -> a
test' Fz = undefined
test' (Fs n) = undefined
}}}
It seems like roughly the same thing as test, but GHC happily accepts the
Fz and Fs constructors. I see now that that is what matching on Nil does
in my original index function, so that is why the seemingly incompatible
Fin constructors are accepted!
Anyway, I promise I'll shut up about this now! It had just misunderstood
how GADT matching actually refined the types. I'm putting this up here for
the benefit of anyone else who might be interested and have the same
confusion (a couple of people in the Haskell IRC channel expressed
interest in my example). Sorry for the noise :)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
