I suppose the actual code may be partly to blame here, in the newer version we now have:
new (I# n#) !b = { etc }
new_ n = new n undefinedElem  which uses `error`
so clearly new_
will always crash at runtime. However versions before GHC 9 did not crash at compiletime.
From https://github.com/haskellari/strictcontainers/runs/2338209240?check_suite_focus=true
[13 of 29] Compiling Data.Strict.HashMap.Autogen.Internal.Strict ( src/Data/Strict/HashMap/Autogen/Internal/Strict.hs, /__w/strictcontainers/strictcontainers/distnewstyle/build/x86_64linux/ghc9.0.1/strictcontainers0.1/build/Data/Strict/HashMap/Autogen/Internal/Strict.o, /__w/strictcontainers/strictcontainers/distnewstyle/build/x86_64linux/ghc9.0.1/strictcontainers0.1/build/Data/Strict/HashMap/Autogen/Internal/Strict.dyn_o )
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
CoreToStg.myCollectArgs
(\ (@v2_aW5m) (@k_aW5k) > case undefinedElem of { })
@v2_aW5m @k_aW5k
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/CoreToStg.hs:938:33 in ghc:GHC.CoreToStg
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
The crash is not transient, it recurs when I rerun the job.
The commit causing the crash only adds a bunch of strictness annotations, though it is operating on a primitive array.
This may or may not be related to #12161, but the code causing the crash here is fairly normal user code.
Consider this code:
data FooState a b c d = FooState
{ partA :: a
, partB :: b
, partC :: c
, partD :: d
}
deriving (Show, Read)
withFoo :: FooState a b c d > FooState a b c d
withFoo = undefined
Eugh, the API has 4 type params. This is confusing for users, especially when they combine it with other functions that take additional type params. In fact (a, b, c, d) are logically "our" (as the author of FooState
) type params, so we can simplify it like this, by grouping them together:
{# LANGUAGE TypeFamilies #}
class FooParams p where
type FooA p
type FooB p
type FooC p
type FooD p
data FooState' p = FooState'
{ partA :: FooA p
, partB :: FooB p
, partC :: FooC p
, partD :: FooD p
}
 deriving (Show, Read)  fails!
withFoo' :: FooParams p => FooState' p > FooState' p
withFoo' = undefined
{# LANGUAGE TypeFamilies, RankNTypes, PolyKinds, DataKinds, StandaloneKindSignatures #}
data FooParams aT bT cT dT = FooParams
{ fooA :: aT
, fooB :: bT
, fooC :: cT
, fooD :: dT
}
type FooA :: forall a b c d. FooParams a b c d > *
type family FooA p where FooA ('FooParams a b c d) = a
type FooB :: forall a b c d. FooParams a b c d > *
type family FooB p where FooB ('FooParams a b c d) = b
type FooC :: forall a b c d. FooParams a b c d > *
type family FooC p where FooC ('FooParams a b c d) = c
type FooD :: forall a b c d. FooParams a b c d > *
type family FooD p where FooD ('FooParams a b c d) = d
data FooState' (p :: FooParams a b c d) = FooState'
{ partA :: FooA p
, partB :: FooB p
, partC :: FooC p
, partD :: FooD p
}
 deriving (Show, Read)  fails!
withFoo' :: FooState' p > FooState' p
withFoo' = undefined
Either way, great, our API now only has 1 type param.
Unfortunately, now deriving (Show, Read)
fails (in both examples):
Test.hs:26:13: error:
• No instance for (Show (FooA p))
arising from the first field of ‘FooState'’ (type ‘FooA p’)
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
• When deriving the instance for (Show (FooState' p))

26  deriving (Show, Read)
 ^^^^
Test.hs:26:19: error:
• No instance for (Read (FooA p))
arising from the first field of ‘FooState'’ (type ‘FooA p’)
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
• When deriving the instance for (Read (FooState' p))

26  deriving (Show, Read)
 ^^^^
We can currently work around this in 2 ways, neither of which is ideal:
{# LANGUAGE TypeFamilies #}
{# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #}
class FooParams p where
type FooA p
type FooB p
type FooC p
type FooD p
data FooState' p = FooState'
{ partA :: FooA p
, partB :: FooB p
, partC :: FooC p
, partD :: FooD p
}
 manually supply the context, eugh
 increases n*m with number of associated types, and the number of extra instances e.g. Eq, Ord
deriving instance (Show (FooA p), Show (FooB p), Show (FooC p), Show (FooD p)) => Show (FooState' p)
deriving instance (Read (FooA p), Read (FooB p), Read (FooC p), Read (FooD p)) => Read (FooState' p)
withFoo' :: FooParams p => FooState' p > FooState' p
withFoo' = undefined
{# LANGUAGE TypeFamilies #}
{# LANGUAGE AllowAmbiguousTypes #}
class FooParams p where
type FooA p
type FooB p
type FooC p
type FooD p
 data decl still has 4 type params
data FooState a b c d = FooState
{ partA :: a
, partB :: b
, partC :: c
, partD :: d
}
deriving (Show, Read)
 apply the type family in a synonym, and expose this along with
 the constructor of the original data type if necessary.
 however, this gets ugly if the data structure is more complex
type FooState'' p = FooState (FooA p) (FooB p) (FooC p) (FooD p)
 API methods can use the type synonym to reduce the number of params
withFoo'' :: FooParams p => FooState'' p > FooState'' p
withFoo'' = undefined
I guess the error is a purposeful design choice to avoid surprising users  the same error occurs if e.g. using IO p
instead of FooA p
, and the same workarounds also work. Clearly, successfully and silently generating an instance with the context (Show (IO p) .. ) =>
, would be surprising to users.
However for certain usecases such as the one I just described, this "potentiallysurprising" derived instance is in fact what we want, and is not surprising for these particular cases (e.g. think Maybe p
). So it would be good if we could override the error and tell GHC to just use what it would have output. This could possibly be implemented as a new strategy with a name such as "stock_relaxed" or "stock_unchecked" or something.
Whoops, yes I do agree that the ignoring should be controllable, I just worded the title of the ticket hastily. (Is ignorable a word?) Thanks for linking the proposal, that is relevant and covers some other things I've wanted too.
Tested with GHC 8.10.1:
I have a toplevel TH splice that looks like this:
thGenerate $ \(~[decl1Rep, decl2Rep]) > [d
decl1 :: ...
decl1 = ... decl1Rep ... decl2Rep ...
decl2 :: ...
decl2 = ... decl1Rep ... decl2Rep ...
]
thGenerate
is implemented using the mfix
from #12073, so it only ever passes a list with the correct amount of elements (e.g. [decl1Rep, decl2Rep]
) into the function given to it on the RHS of the expression. Of course I don't expect the compiler to be able to figure this out, but it would be good to have a flag to suppress the warning generated  the code is run at compiletime, so the warning is not relevant to any runtime event or condition.
Currently I can suppress the warning using Wnoincompleteunipatterns
, but this also suppresses regular warnings for runtime code.
Note that this is different from #14838 which talks about generated code (e.g. in the [d ... ]
on the RHS of the expression. Those warnings precisely should not be suppressed as part of this ticket, since they are for code that runs at runtime.
Note that this is also different from the suggestion in this comment which again is about code that runs at runtime.
This ticket is only about code that is run at compile time (by the TH splicer), that does not itself run at runtime.
(Pretty sure this is different from #14633 where the function actually was ambiguous.)
Tested on GHC 8.10.1:
{# LANGUAGE DefaultSignatures #}
{# OPTIONS_GHC Werror Wredundantconstraints #}
class Base a where
myList :: [a]
default myList :: SubClass a => [a]
myList = defaultMyList
class Base a => SubClass a where
myList2 :: [a]
defaultMyList :: SubClass a => [a]
defaultMyList = myList2
main :: IO ()
main = pure ()
The error is as follows:
Test.hs:7:11: error: [Wredundantconstraints, Werror=redundantconstraints]
• Redundant constraint: Base a
• In the type signature for:
myList :: forall a. (Base a, SubClass a) => [a]
In the ambiguity check for ‘myList’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method: myList :: forall a. Base a => [a]

7  default myList :: SubClass a => [a]
 ^^^^^^
suggesting that some automatic process is adding (Base a)
as an implicit constraint, but then this redundancy check is failing on the automaticallyadded constraint  which it shouldn't because the programmer can't do anything about it.
Adding AllowAmbiguousTypes
does make the error go away, as the error message suggests, however the type is not ambiguous  there is no falsepositive for defaultMyList
with the same (sourcelevel) signature. Adding ConstrainedClassMethods
makes no difference.
On second thoughts, I've figured out how to use MonadFix
correctly, so this is not necessary (for my usecase) once #12073 (closed) is done. The key point is that splicing $(myFunc')
inside the function counts as "evaluating" it for the purpose of mfix
, and that is where the infinite loop was coming from.
Refactoring generateExtras
to instead have type signature ([Exp] > Q [Dec]) > Q [Dec]
with an internal usage of mfix (f :: ([Exp] > Q [Exp]))
works without resulting in an infinite loop, then one has to splice $(pure myFunc')
etc..
I want to write something like:
$(generateExtras
[d myFunc :: T ]
(\(~[myFunc']) > [d myFunc = ... $(myFunc') ... ]))
where generateExtras
generates myFunc'
from the typesignature of myFunc
, and passes it to be used in the RHS of the definition of myFunc
. However the above code causes GHC to complain about "type signature for 'myFunc' lacks an accompanying binding".
OTOH, writing the Q Dec
instance manually works:
$(generateExtras
(pure <$> sigD (mkName "myFunc") [t Int ])
(\(~[myFunc']) > [d myFunc = ... $(myFunc') ... ]))
so it seems reasonable that the [d..]
quasiquoted version should also succeed.
(Actually, as an aside, in case this was a XY problem, ideally I'd write something like the following:
$(generateExtras $ \(~[myFunc']) > [d
myFunc :: T
myFunc = ... $(myFunc') ...
but even using the MonadFix
instance from #12073 and being very careful in the implementation of generateExtras
not to patternmatch on the RHS of any nonSigD
declarations, causes an infinite loop during compilation. :()
Actually I take that back, it relies on the SEq
instance for Symbol
not Type
so it indeed doesn't need the workaround, yay!
(or more accurately, as discussed above, reuses singleton's wrappedup use of unsafeCoerce
inside the SEq
)
Thanks! Ryan & I continued the discussion on the singletons issue and eventually I was able to rewrite the code in a form that doesn't need the unsafeCoerce
workaround. :)
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 Wincompletepatterns #}
{
The code includes the following things:
* Proving a multipart 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 toplevel due to
 https://github.com/goldfirere/singletons/issues/339#issuecomment612530482
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 / templatehaskell 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 nonexhaustive
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 "staticallytyped lookup" $ withLookupKV v k0 c
withSomeSing (pack "a") $ \k > do
prints "dynamicallytyped 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 "dynamicallytyped lookup" $ withLookupKV v k0 c
Please see withLookupKV2
 if we comment the TNothing
branch, with Wincompletepatterns
we get:
kvlist.hs:172:14: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
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: [Winaccessiblecode]
• 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 patternmatching 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.
Continuing at https://github.com/goldfirere/singletons/issues/447
With GHC 8.8.3:
Test.hs
{# LANGUAGE GADTs, TypeFamilies, PolyKinds, DataKinds, ConstraintKinds, TypeOperators, PolyKinds,
RankNTypes, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
UndecidableInstances, LambdaCase, EmptyCase, TypeFamilyDependencies #}
import Data.Kind
import GHC.TypeLits
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Singletons.Decide
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t > TMaybe ('Just t)
data KVList (kk :: [Symbol]) (vv :: [Type]) :: Type where
KVNil :: KVList '[] '[]
KVCons :: !(Sing k) > !v > !(KVList kk vv) > KVList (k : kk) (v : vv)
type family LookupKV (k :: Symbol) (tab :: Type) = v where
LookupKV k (KVList '[] '[]) = TMaybe 'Nothing
LookupKV k (KVList (k ': kk1) (v ': vv1)) = TMaybe ('Just v)
LookupKV k (KVList (k1 ': kk1) (v ': vv1)) = LookupKV k (KVList kk1 vv1)
lookupKV
:: Sing k > KVList kk vv > LookupKV k (KVList kk vv)
lookupKV k = \case
KVNil > TNothing
KVCons k' v r > case k %~ k' of
Proved Refl > TJust v
Disproved d > lookupKV k r
The last line gives:
• Could not deduce: LookupKV k (KVList kk1 vv1)
~ LookupKV k (KVList (k1 : kk1) (v : vv1))
from the context: (kk ~ (k1 : kk1), vv ~ (v : vv1))
bound by a pattern with constructor:
KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
Sing k > v > KVList kk vv > KVList (k : kk) (v : vv),
in a case alternative
at Test.hs:28:315
Expected type: Decision (LookupKV k (KVList kk vv))
Actual type: Decision (LookupKV k (KVList kk1 vv1))
With fprintexplicitkinds
:
• Could not deduce: (LookupKV k (KVList kk1 vv1) :: *)
~ (LookupKV k (KVList ((':) @Symbol k1 kk1) ((':) @* v vv1)) :: *)
from the context: ((kk :: [Symbol])
~ ((':) @Symbol k1 kk1 :: [Symbol]),
(vv :: [*]) ~ ((':) @* v vv1 :: [*]))
bound by a pattern with constructor:
KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
Sing @Symbol k
> v > KVList kk vv > KVList ((':) @Symbol k kk) ((':) @* v vv),
in a case alternative
at Test.hs:28:315
which doesn't seem to raise anything suspicious, all the kinds are fullyresolved and contain no variables that could be ambiguous.
But in the definition for type family LookupKV
it specifically says
LookupKV k (KVList (_ ': kk) (v ': vv)) = LookupKV k (KVList kk vv)
Considering the fact the Proved (TJust v)
branch typechecks, GHC must have deduced LookupKV k (KVList (k ': kk1) (v ': vv1)) ~ TMaybe ('Just v)
via the corresponding typefamily rule. So it's strange it doesn't use another typefamily rule for this unsatisfied deduction. I'm pretty sure this is unrelated to injectivity since k, kk, and vv all appear as themselves in the actual type signature, unapplied to a type family.
Ok, will do!
(This is getting into the realms of singletons territory, please let me know if it would be better to move this to the singletons bug tracker.)
I figured out how to rewrite the above code to avoid unsafeCoerce
, using SEq
as you said instead of SDecide
 so I guess it is possible to avoid unsafeCoerce
in user code as you say, as long as you know how to appropriately use singletons. However please read further below:
{# LANGUAGE ConstraintKinds, DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #}
import Data.Kind
import Data.Singletons.Decide
import Data.Singletons.Prelude
import Data.Singletons.TH
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t > TMaybe ('Just t)
data KVList (kk :: [kt]) (vv :: [Type]) :: Type where
KVNil :: KVList '[] '[]
KVCons :: !(Sing (k :: kt)) > !(v :: Type) > !(KVList kk vv) > KVList (k : kk) (v : vv)
singletons [d
lookupKV :: Eq k => k > [k] > [v] > Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v:vv) = if k == k' then Just v else lookupKV k kk 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
 This version doesn't typecheck!
 It's similar to the one in the original post, except
 it uses singleton's autogenerated LookupKV type family
 instead of the manuallywritten one.
hLookupKV'
:: SDecide 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
Proved Refl > TJust v
Disproved _ > hLookupKV' sk rem
 ^ even unsafeCoerce doesn't help, we are still left with "could not deduce" errors
The whole situation is very confusing  as you can see, the difference between the working and nonworking versions are solely down to the choice of SEq
vs SDecide
. I suppose you would understand why, but could this please be added to the documentation? SEq
would seem to fit better into the rest of the singletons framework, so now I don't understand the purpose of having a separate SDecide
, especially if it works less well (at least here) than SEq
.
Another thing that is confusing, is that the implementation for DefaultEq
seems to do the very thing I did at the top where you have an overlapping type family declaration, yet somehow it works for singletons. (The unsafeCoerce
workaround you cited is only for SEq Type
whereas DefaultEq
is used for most other types/kinds, it would seem.)
Ok, great thanks all for the explanations & the workaround suggestion. I just found this exact issue documented at the haskell wiki including the situation with GADT match, sorry for not finding it earlier. As it states, "The only general way to fix this is to have inequality evidence introduced into GHC, and that's a big deal and we don't know if we have the motivation for such a change yet."
But does this issue need to be resolved, before dependent types can progress further in GHC? If I understood correctly, singletons
can get away with a single use of unsafeCoerce
in SEq
as it only provides typelevel functions, but if one wants to write a dependent function like I'm doing here that matches on values, one will have to use %~
which likely will cause this error and force the workaround  and so a lot of different people writing dependent functions might end up having to use unsafeCoerce
, rather than it being just in a single place in a wellmaintained and carefullyreasoned library. I am not sure if it's possible to "wrap up" the logic of this workaround and provide it as a safe utility function.
I see, thanks in that case I'll use unsafeCoerce
as a workaround as well then.
all it has is
(b1 :~: b2) > Void
, which is a simple, intuistionistic encoding of type inequality
I'm just wildly conjecturing here, but couldn't this be used as a nonfirstclass witness of type inequality  so when @simonpj says "it can't use (3) until it's certain that (2) does not apply", it could be certain when it has a (b1 :~: b2) > Void
in scope. Or would that be too specific / inelegant to achieve in practice in the deduction algorithm, which has to be general?
Arguably it is also too easy to fake an incorrect (b1 :~: b2) > Void
especially when Wincompletepatterns
is off, so I could understand if this suggestion would be unsound or otherwise inappropriate.
That could make sense, however in the case match on k %~ k'
this returns a Decision (k :~: k')
which is Disproved
in the recursive branch  so isn't this sufficient evidence that k
and k1
are "apart"? (Although I appreciate Decision
is a singletons construct, so perhaps GHC does not make use of it.)