GHC's behavior is strange on this code

narrowed-down.hs

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
module Main(main) where

import Data.Proxy

class Same x y where
  cast :: Proxy x -> Proxy y

class Impossible x y where
  impossible :: Proxy x -> Proxy y

instance {-# INCOHERENT #-} Same x x where
  cast = id

instance {-# INCOHERENT #-} Impossible x y => Same x y where
  cast = impossible

{-

I realized I misunderstood my code above.

I forgot Haskell's constraint solving does not "backtrack" and made a mistake.
Above instance declaration means,

> Try to unify against (Same x x) or (Same x y) in *undetermined* order. For first time
> it successfully unify, try to solve their constraint.

So depending on context, solving constraint `(Same x x) =>` may or may not succeed.
It's hardly a correct program. Similarly, my first program (strange-typecheck.hs) was
already incorrect, and randomly failed as it was supposed to.

-}

wrap :: (forall y. Proxy y -> a) -> a
wrap f = f Proxy

-- Compiles
example1 :: forall x. Proxy x -> Proxy x
example1 px = let px' = wrap (const px) in cast px'

-- Compile Error
example2 :: forall x. Proxy x -> Proxy x
example2 px = case wrap (const px) of px' -> cast px'

---------------------------------

main :: IO ()
main = putStrLn "compiles"

reported_error.txt

strange-typecheck.hs:34:54: error:
    • No instance for (Has x ()) arising from a use of ‘use’
    • In the expression: use px' 1
      In a case alternative: Tag px' -> use px' 1
      In the expression:
        case (boundary $ \ py -> use py px) of { Tag px' -> use px' 1 }
   |
34 |     case (boundary $ \py -> use py px) of Tag px' -> use px' 1
   |                                                      ^^^^^^^^^

strange-typecheck.hs

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
module Main(main) where

import Data.Proxy

newtype Tag a b = Tag { unTag :: b }
  deriving (Show)

boundary :: (forall x. Proxy x -> Tag (x, xs) a) -> Tag xs a
boundary f = Tag . unTag $ f Proxy

class Has x xs

instance {-# INCOHERENT #-} Has x (x, xs)
instance {-# INCOHERENT #-} Has x xs => Has x (y, xs)

use :: Has x xs => Proxy x -> a -> Tag xs a
use _ = Tag

-- This compiles
good :: Tag () Int
good =
  boundary $ \px ->
    let taggedPx = boundary $ \py -> use py px
    in case taggedPx of Tag px' -> use px' 1

-- This does not
bad :: Tag () Int
bad =
  boundary $ \px ->
    case (boundary $ \py -> use py px) of Tag px' -> use px' 1

main :: IO ()
main = putStrLn "compiles"