How to make GHC to type-check the last branch of pop ?
GHC understands that x == c in Just Refl case,
but it cannon unify default branch with last type family case.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
import Prelude
import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality
data N (l :: [Symbol]) where
NilN :: () -> N '[]
ConsN :: KnownSymbol x => Proxy x -> N l -> N (x : l)
type family Pop n c where
Pop '[] _ = '[]
Pop (c ': n) c = n
Pop m c = m
pop :: forall c n. KnownSymbol c => N n -> Proxy c -> N (Pop n c)
pop (NilN ()) _ = NilN ()
pop l@(ConsN x n) c =
case sameSymbol x c of
Just Refl -> n
Nothing -> l
Could not deduce ‘Pop (x : l) c ~ (x : l)’
from the context: (n ~ (x : l), KnownSymbol x)
bound by a pattern with constructor:
ConsN :: forall (x :: Symbol) (l :: [Symbol]).
KnownSymbol x =>
Proxy x -> N l -> N (x : l),
in an equation for ‘pop’
This is indeed difficult, unfortunately. It’s been discussed by the GHC developers a few times over the years, see in particular this ticket and those linking to it:
In Agda you would write it like this (I’ve used Char instead of String because that felt simpler while still presenting the same problems):
open import Data.Char
open import Data.List
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality
data N : List Char → Set where
[] : N []
_∷_ : ∀{xs} → (x : Char) → N xs → N (x ∷ xs)
popHelper : {a : Set} → Dec a → List Char → List Char → List Char
popHelper (yes _) _ n = n
popHelper (no _) l _ = l
pop : (n : List Char) (c : Char) → List Char
pop [] _ = []
pop l@(x ∷ n) c = popHelper (x ≟ c) l n
popNHelper : ∀ {xs x c} (w : Dec (x ≡ c)) → N (x ∷ xs) → N xs → N (popHelper w (x ∷ xs) xs)
popNHelper (yes _) _ n = n
popNHelper (no _) l _ = l
popN : ∀{n} → N n → (c : Char) → N (pop n c)
popN [] _ = []
popN l@(x ∷ n) c = popNHelper (x ≟ c) l n
They also use this Dec type instead of Maybe which includes an explicit proof of refutation:
data Dec (a : Set) : Set where
yes : a → Dec a
no : (a → ⊥) → Dec a
But I don’t think that’s very relevant here. I think a more important problem is the nonlinear matching that type families allow you to do. This is not allowed in Agda and in my opinion questionable in general.
Here is a trick: instead of defining Pop with non-linear patterns in the equality case, you branch on a boolean equality test:
type family Pop n c where
Pop '[] _ = '[]
Pop (d ': n) c = If (d == c) n (d ': n)
Then in the pop function you need to match on this boolean. From a KnownSymbol constraint, there is no way to do this safely AFAIK, so here is a way that defines the missing primitive eqSymbol using unsafeCoerce:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Prelude
import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Unsafe.Coerce (unsafeCoerce)
data N (l :: [Symbol]) where
NilN :: () -> N '[]
ConsN :: KnownSymbol x => Proxy x -> N l -> N (x : l)
type family Pop n c where
Pop '[] _ = '[]
Pop (d ': n) c = If (d == c) n (d ': n)
pop :: forall c n. KnownSymbol c => N n -> Proxy c -> N (Pop n c)
pop (NilN ()) _ = NilN ()
pop l@(ConsN x n) c =
case eqSymbol x c of
STrue -> n
SFalse -> l
data SBool (b :: Bool) where
STrue :: SBool True
SFalse :: SBool False
eqSymbol :: (KnownSymbol c, KnownSymbol d) => Proxy c -> Proxy d -> SBool (c == d)
eqSymbol c d = case sameSymbol c d of
Just Refl -> unsafeCoerce STrue -- can't solve (c == c) ~ True ???
Nothing -> unsafeCoerce SFalse
main :: IO ()
main = pure ()
The issue with Just Refl -> STrue is due to a weird definition of == in base (I guess it can’t decide it isn’t in the first case); it will go away if you define == the obvious way.
You can also replace eqSymbol with a smaller, more general apart primitive, allowing you to write the second pop case like so.
pop l@(ConsN x n) c = case decideSymbol x c of
Left (apart -> Refl) -> l
Right Refl -> n
I tried solutions from @Lysxia and @Leary.
Thanks a lot, I totally missed the coerce hammer option!
The original attempt checks if I just put unsafeCoerce in the last branch. Without If typefamily UndecidableInstances can be turned off.
type family Pop n c where
Pop '[] _ = '[]
Pop (c ': n) c = n
Pop m c = m
pop :: forall c n. KnownSymbol c => N n -> Proxy c -> N (Pop n c)
pop (NilN ()) _ = NilN ()
pop l@(ConsN x n) c =
case sameSymbol x c of
Just Refl -> n
Nothing -> unsafeCoerce l
The reason for its weird implementation is discussed in this comment.
Rather than simplifying it, the better course of action should be to use/provide:
equal :: a :~: b -> (a == b) :~: True
equal Refl = unsafeCoerce (Refl @True)
apart
I didn’t do enough testing. There’s no issue with this primitive in principle, but in practice the GHC.TypeLits.decide* functions don’t actually provide legitimate inequalities. apart refuses to be fooled and explodes.