[GHC] #15909: prepareAlts does not take into account equalities which are in scope

16 Nov 2018

      #15909: prepareAlts does not take into account equalities which are in scope
-------------------------------------+-------------------------------------
           Reporter:  mpickering     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15909>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler