Contradictory warnings between -Winaccessible-code and -Wincomplete-patterns under GADT pattern-match with constraints
The code is a bit long but hopefully not too complex to follow; I can try to minimise it on request. It uses singletons but I don't think it's related to the library, since the warnings clearly contradict each other:
With GHC 8.8.3:
{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,
GADTs, LambdaCase, MultiParamTypeClasses, RankNTypes, PolyKinds, ScopedTypeVariables,
TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-
The code includes the following things:
* Proving a multi-part theorem via constraints, slightly more complex than
the ones in ../regexp.
* Generating the proof constraint automatically, when GHC isn't able to -
e.g. for an untouchable (runtime) type underneath 'withSomeSing'.
* Use of the proof to statically rule out more complex consequences such as
relating two lookups of two different data structures.
* Using utility functions that require the proof, on a runtime type.
* Workarounds for some singletons issues / idosyncracies.
-}
import Data.Foldable (traverse_)
import Data.Text (pack)
import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
singletons [d|
-- note: subexpressions are lifted out to the top-level due to
-- https://github.com/goldfirere/singletons/issues/339#issuecomment-612530482
lookupKV :: Eq k => k -> [k] -> [v] -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v:vv) = lookupKV_If k kk v vv (k == k')
lookupKV_If :: Eq k => k -> [k] -> v -> [v] -> Bool -> Maybe v
lookupKV_If _ _ v _ True = Just v
lookupKV_If k kk v vv False = lookupKV k kk vv
|]
{- Proof that fmap f (lookupKV k kk vv) == lookupKV k kk (fmap f vv)
The proof roughly follows the below structure, modulo the fact that we split
out lookupKV into 2 functions due to a singletons / template-haskell issue,
discussed in the link above.
Inducting on kk vv:
Given:
Wf. (Fmap f (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv))
Sf. Just (Apply f v') ~ Fmap f (Just v')
Tf. Apply f v' ': Fmap f vv ~ Fmap f (v' ': vv)
Deduce:
(Fmap f (LookupKV k (k' ': kk) (v' ': vv)) ~ LookupKV k (k' ': kk) (Fmap f (v' ': vv)))
by (Tf), ~
LookupKV k (k' ': kk) (Apply f v' ': Fmap f vv)
if k == k' if k == k'
then -> Fmap f (Just v') by (Sf) ~ then -> Just (Apply f v')
else -> Fmap f (LookupKV k kk vv) by (Wf) ~ else -> Lookup k kk (Fmap f vv)
[].
Note that GHC deduces Sf and Tf automatically, so they don't need to appear
explicitly in the code proof below.
-}
class (Fmap f (LookupKV k kk vv) ~
LookupKV k kk (Fmap f vv))
=> ProofLookupKV f k (kk :: [kt]) vv where
instance -- base case
ProofLookupKV f k '[] '[]
instance -- implicit (Apply f v' ': Fmap f vv ~ Fmap f (v' ': vv)) =>
(ProofLookupKV_If f k k' kk v' vv (k == k'))
=> ProofLookupKV f (k :: kt) (k' ': kk) (v' ': vv)
class (Fmap f (LookupKV_If k kk v' vv eq) ~
LookupKV_If k kk (Apply f v') (Fmap f vv) eq)
=> ProofLookupKV_If f (k :: kt) k' kk v' vv eq where
instance -- implicit (Just (Apply f v') ~ Fmap f (Just v')) =>
ProofLookupKV_If f k k' kk v' vv 'True -- Just v
instance
ProofLookupKV f k kk vv
=> ProofLookupKV_If f k k' kk v' vv 'False -- lookupKV kk vv
-- | Prove @ProofLookupKV f k kk vv@ and supply it to a context that needs it.
--
-- Use this when GHC can't automatically deduce it. For example, you need this
-- inside a @withSomeSing@ and other similar things involving a runtime 'k'.
--
-- You will likely have to supply the correct @f@, which you can probably get
-- from the error message.
withSomeProofLookupKV
:: forall kt f (k :: kt) (kk :: [kt]) vv r
. SEq kt
=> Sing k
-> KVList kk vv
-> (ProofLookupKV f k kk vv => r)
-> r
withSomeProofLookupKV k KVNil c = c
withSomeProofLookupKV k (KVCons k' v tab) c = case k %== k' of
STrue -> withSomeProofLookupKV @_ @f k tab c
SFalse -> withSomeProofLookupKV @_ @f k tab c
-------------------------------------------------------------------------------
-- Heterogeneous map implementation
-- heterogeneous Maybe that carries the type
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t -> TMaybe ('Just t)
-- heterogeneous association list
--
-- @kk@ is kept separately for easier unification with other lists
data KVList (kk :: [kt]) (vv :: [Type]) :: Type where
KVNil :: KVList '[] '[]
KVCons :: !(Sing (k :: kt)) -> !(v :: Type) -> !(KVList kk vv) -> KVList (k : kk) (v : vv)
hLookupKV
:: SEq kt
=> Sing (k :: kt)
-> KVList (kk :: [kt]) vv
-> TMaybe (LookupKV k kk vv)
hLookupKV sk KVNil = TNothing
hLookupKV sk (KVCons sk'' v rem) = case sk %== sk'' of
STrue -> TJust v
SFalse -> hLookupKV sk rem
-- | Version of 'hLookupKV' that inlines the proof, so we don't perform the
-- lookup twice like if we wrapped 'withSomeProofLookupKV' around it.
hLookupKVWithProof
:: forall kt f (k :: kt) (kk :: [kt]) vv r
. SEq kt
=> Sing k
-> KVList kk vv
-> (ProofLookupKV f k kk vv => TMaybe (LookupKV k kk vv) -> r)
-> r
hLookupKVWithProof sk KVNil f = f TNothing
hLookupKVWithProof sk (KVCons sk'' v rem) f = case sk %== sk'' of
STrue -> f (TJust v)
SFalse -> hLookupKVWithProof @kt @f sk rem f
withLookupKV
:: forall (k :: kt) kk vv r
. SEq kt
=> ProofLookupKV (FlipSym2 (TyCon2 (->)) r) k kk vv
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV tab k conts = case hLookupKV k tab of
TNothing -> Nothing
TJust v -> case hLookupKV k conts of
-- GHC statically knows this can't be TNothing due to ProofLookupKV constraint
TJust cont -> Just (cont v)
withLookupKV2
:: forall (k :: kt) kk vv r
. SEq kt
=> KVList (kk :: [kt]) vv
-> Sing k
-> KVList (kk :: [kt]) (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
withLookupKV2 tab k conts = hLookupKVWithProof @kt @(FlipSym2 (TyCon2 (->)) r) k tab $ \case
TNothing -> Nothing
TJust v -> case hLookupKV k conts of
-- TNothing -> Nothing -- if uncommented, gives • Couldn't match type ‘'Just (t -> r)’ with ‘'Nothing’
-- if commented, gives Pattern match(es) are non-exhaustive
TJust cont -> Just (cont v)
main :: IO ()
main = do
let k0 = SSym @"a"
let k1 = SSym @"b"
let v = KVCons k0 (3 :: Int) $ KVCons k1 "test" $ KVNil
let c = KVCons k0 (show . (+) (2 :: Int)) $ KVCons k1 (<> "ing") $ KVNil
let prints pre = traverse_ (putStrLn . (\s -> pre <> ": " <> s))
prints "statically-typed lookup" $ withLookupKV v k0 c
withSomeSing (pack "a") $ \k -> do
prints "dynamically-typed lookup, inlined proof" $ withLookupKV2 v k0 c
-- without this line, GHC fails with:
-- No instance for (ProofLookupKV_If (FlipSym2 (TyCon2 (->)) [Char]) {..etc..} (DefaultEq a "a"))
-- arising from a use of ‘withLookupKV’
withSomeProofLookupKV @_ @(FlipSym2 (TyCon2 (->)) [Char]) k v $ do
prints "dynamically-typed lookup" $ withLookupKV v k0 cPlease see withLookupKV2 - if we comment the TNothing branch, with -Wincomplete-patterns we get:
kvlist.hs:172:14: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: TNothing
|
172 | TJust v -> case hLookupKV k conts of
| ^^^^^^^^^^^^^^^^^^^^^^^^^...OTOH if we uncomment the line, we get:
kvlist.hs:173:5: warning: [-Winaccessible-code]
• Couldn't match type ‘'Just (t -> r)’ with ‘'Nothing’
Inaccessible code in
a pattern with constructor: TNothing :: forall k. TMaybe 'Nothing,
in a case alternative
• In the pattern: TNothing
In a case alternative: TNothing -> Nothing
In the expression:
case hLookupKV k conts of
TNothing -> Nothing
TJust cont -> Just (cont v)
• Relevant bindings include
v :: t (bound at kvlist.hs:172:9)
conts :: KVList kk (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
(bound at kvlist.hs:170:21)
withLookupKV2 :: KVList kk vv
-> Sing k
-> KVList kk (Fmap (FlipSym2 (TyCon2 (->)) r) vv)
-> Maybe r
(bound at kvlist.hs:170:1)
|
173 | TNothing -> Nothing -- if uncommented, gives • Couldn't match type ‘'Just (t -> r)’ with ‘'Nothing’
| ^^^^^^^^Note that the other function that does the same thing, but has an explicit external constraint, withLookupKV, is fine.
I saw a lot of issues relating to pattern-matching and exhaustion checking and there is even a wiki page about it, but couldn't find an open duplicate. I also couldn't find a duplicate relating to inaccessible code. Of course it's just a minor annoyance involving warnings, I can live with it in the meantime.