prepareAlts does not take into account equalities which are in scope

If we consider this program submitted for our consideration by Andres we see some surprising behaviour.

https://gist.github.com/kosmikus/237946a2335600690208a4a36efef988

{-# LANGUAGE TypeOperators, GADTs, FlexibleContexts, DataKinds, RankNTypes, PolyKinds, TypeFamilies, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperClasses, FlexibleInstances, ConstraintKinds, TypeApplications, EmptyCase, ScopedTypeVariables, PartialTypeSignatures, TemplateHaskell #-}
module Partition where

import Data.Coerce
import Data.Kind
import Data.Proxy

data NP (f :: k -> Type) (xs :: [k]) where
  Nil :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x : xs)

infixr 5 :*

strictToPair :: forall f a b . NP f '[a, b] -> (f a, f b)
strictToPair np =
  case np of
    (fx :* fxs) ->
      case (fxs {- :: NP f '[b] -}) of
        (fy :* fys) ->
          (fx, fy)

Both pattern matches are exhaustive so we don't need to generate any failure cases when pattern matching.

Notice in the generated core that we have a match on Partition.Nil even though the match will never be reached.

 Partition.strictToPair                                                          
  :: forall k (f :: k -> *) (a :: k) (b :: k).                                  
      Partition.NP f '[a, b] -> (f a, f b)                                       
 [GblId, Arity=1, Str=<S,1*U>m, Unf=OtherCon []]                                 
 Partition.strictToPair                                                          
   = \ (@ k_a1gV)                                                                
       (@ (f_a1gW :: k_a1gV -> *))                                               
       (@ (a_a1gX :: k_a1gV))                                                    
       (@ (b_a1gY :: k_a1gV))                                                    
       (np_s1yz [Occ=Once!] :: Partition.NP f_a1gW '[a_a1gX, b_a1gY]) ->         
       case np_s1yz of                                                           
       { Partition.:* @ x_a1h2 @ xs_a1h3 co_a1h4 fx_s1yB [Occ=Once]              
                      fxs_s1yC [Occ=Once!] ->                                    
       case fxs_s1yC of {                                                        
         Partition.Nil _ [Occ=Dead, Dmd=<B,A>] ->                                
           Partition.strictToPair1 @ k_a1gV @ a_a1gX @ f_a1gW @ b_a1gY;          
         Partition.:* @ x1_a1h7 @ xs1_a1h8 co1_a1h9 fy_s1yE [Occ=Once]           
                      _ [Occ=Dead] ->                                            
           (fx_s1yB                                                              
            `cast` (<f_a1gW>_R (Nth:1 (Sym co_a1h4))                             
                    :: (f_a1gW x_a1h2 :: *) ~R# (f_a1gW a_a1gX :: *)),           
            fy_s1yE                                                              
            `cast` (<f_a1gW>_R (Nth:1 (Sym co1_a1h9 ; Nth:2 (Sym co_a1h4)))      
                   :: (f_a1gW x1_a1h7 :: *) ~R# (f_a1gW b_a1gY :: *)))          
       }                                                                         
      } 

This is because in prepareAlts are try to inspect the type of fxs which looks like a type variable, however it has since been refined by the pattern match on np above. Adding the explicit type signature to fxs makes prepareAlts treat it correctly.

Trac metadata

Trac field	Value
Version	8.6.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture