#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=