#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