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

changed milestone to %8.6.3

changed weight to 5

added Tbug Trac import labels

Here is a much simpler example which demonstrates the issue:

{-# LANGUAGE GADTs #-}
module Bug where

data T a where
  TInt  :: T Int
  TBool :: T Bool

f1 :: T Int -> ()
f1 TInt = ()

f2 :: a ~ Int => T a -> ()
f2 TInt = ()

$ /opt/ghc/8.6.2/bin/ghc Bug.hs -O2 -ddump-simpl
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

==================== Tidy Core ====================
...
f1
  = \ (ds_d1tE :: T Int) ->
      case ds_d1tE of { TInt co_a1s1 [Dmd=<L,A>] -> GHC.Tuple.() }
...
f2
  = \ (@ a_a1rU) _ [Occ=Dead] (ds_d1tf :: T a_a1rU) ->
      case ds_d1tf of {
        TInt co_a1rX [Dmd=<L,A>] -> GHC.Tuple.();
        TBool ipv_s1tT [Dmd=<B,A>] -> Bug.f4
      }

Bug.f4
  = Control.Exception.Base.patError
      @ 'GHC.Types.LiftedRep @ () lvl_r1v7

Reasoning about equalities is the business of the typechecker, and the simplifier doesn't do much.

But it does do some things; e.g. it tries to reduce type-family applications.

It would be reasonable to try to make it do more; and indeed to support the pattern-match overlap stuff we have an API for the typechecker that can be called externally. I don't know if it's the right API for this purpose.

To make this work we'd have to accumulate the "givens" as we go down. Not too hard. I'd be inclined to do this in a separate pass, NOT the simplifier which has too much else to do. Just possibly the occurrence analyser, though I worry about slowing it down.

Another tricky point is that I'd like to be able to prove that every case is exhaustive, and a Lint-checkable property. But if I later remove the second parameter to f2 (it is dead) then it won't be provable anymore. This problem is more basic than fancy equalities. Consider

case x of
  Red -> e1
  DEFAULT -> let v = case x of 
                       Red -> e2
                       Blue -> e3
                       Green -> e4
             in blah

we can prune the Red branch out of the case in the RHS of v. But now imagine floating the v-binding:

let v = case x of 
          Blue -> e3
          Green -> e4
in case x of
  Red -> e1
  DEFAULT -> blah

This is actually still correct, but it's not obviously correct.

Ticket retargeted after milestone closed

added Pnormal label