Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable
Consider this program,
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Test where
import GHC.Exts
import Data.Kind
data TypeRep (a :: k) where
Con :: TypeRep (a :: k)
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
TypeRep a
-> TypeRep b
-> TypeRep (a -> b)
pattern Fun :: forall k (fun :: k). ()
=> forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(arg :: TYPE r1) (res :: TYPE r2).
(k ~ Type, fun ~~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern Fun arg res <- TrFun arg res
where Fun arg res = undefined
data Dynamic where
Dynamic :: forall a. TypeRep a -> a -> Dynamic
-- Removing this allows compilation to proceed
{-# COMPLETE Con #-}
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
-- Changing Fun to TrFun allows compilation to proceed
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
dynApply _ _ = Nothing
As written the program fails with,
test.hs:34:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘dynApply’:
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...
|
34 | dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This can be worked around by doing one of the following,
- Removing the
COMPLETE
pragma - Changing the use of the
Fun
pattern synonym into a use of theTrFun
constructor.
Something is quite wrong here.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | George |
Operating system | |
Architecture |