Skip to content

`Could not match 'Many with 'Many` recurring whenever there's an error

Summary

I'm getting some really weird error messages when there's an error in my module, the error messages just reoccur, no matter where the actual error is.

instance (forall x. Eq x => Eq (f x), Typeable f) => Eq (ETree (Has (Both Typeable Eq) f)) where
  ex == ey =
    with2 ex \x -> with2 ey \y ->
      case (x, y) of
        (HNode (Proves m) ms, HNode (Proves n) ns) ->
          case eqTypeRep (typeOf m) (typeOf n) of
            Nothing -> False
            Just HRefl -> m == n && go ms ns
   where
    -- go :: forall xs ys. HList (HTree (Has (Both Typeable Eq) f)) xs -> HList (HTree (Has (Both Typeable Eq) f)) ys -> Bool
    go ms ns =
      case (ms, ns) of
        (HNil, HNil) -> True
        (HCons m' ms', HCons n' ns') -> MkSome2 m' == MkSome2 n' && go ms' ns'
        (_, _) -> False

If I put in the commented out line, it builds just fine, if not, I get errors, the first being:

htree> src/Data/HTree/Existential.hs:116:27: error: [GHC-18872]
htree>     • Couldn't match type ‘Many’ with ‘Many’
htree>         arising from multiplicity of ‘ms’
htree>     • In the pattern: HNode (Proves m) ms
htree>       In the pattern: (HNode (Proves m) ms, HNode (Proves n) ns)
htree>       In a case alternative:
htree>           (HNode (Proves m) ms, HNode (Proves n) ns)
htree>             -> case eqTypeRep (typeOf m) (typeOf n) of
htree>                  Nothing -> False
htree>                  Just HRefl -> m == n && go ms ns
htree>     |
htree> 116 |         (HNode (Proves m) ms, HNode (Proves n) ns) ->
htree>     |                           ^^
htree> src/Data/HTree/Existential.hs:116:48: error: [GHC-18872]
htree>     • Couldn't match type ‘Many’ with ‘Many’
htree>         arising from multiplicity of ‘ns’
htree>     • In the pattern: HNode (Proves n) ns
htree>       In the pattern: (HNode (Proves m) ms, HNode (Proves n) ns)
htree>       In a case alternative:
htree>           (HNode (Proves m) ms, HNode (Proves n) ns)
htree>             -> case eqTypeRep (typeOf m) (typeOf n) of
htree>                  Nothing -> False
htree>                  Just HRefl -> m == n && go ms ns
htree>     |
htree> 116 |         (HNode (Proves m) ms, HNode (Proves n) ns) ->
htree>     |                                                ^^

This is especially weird because I don't even have -XLinearTypes enabled.

Steps to reproduce

  • nix build sourcehut:~mangoiv/htree/d17ea9939d88aa2fc522943d8b23aca43098c12b#package-96 (or 92/94)
  • or clone this repo: https://git.sr.ht/~mangoiv/htree, checkout d17ea9939d88aa2fc522943d8b23aca43098c12b, cabal build

Expected behavior

don't tell me that 'Many and 'Many aren't the same

Environment

  • GHC version used: ghc 927, 944 and 961

Optional:

  • Operating System: NixOS 23.05
  • System Architecture: x86_64-linux
Edited by Magnus
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information