# Why in some cases some come works when pattern matching via case-of, but not via a let binding?

I'm trying to understand singletons. As an exercise I'm manually defining an instance of `SingKind` for a custom `List` type:

``````data List a = Nil | Cons a (List a)

data SList :: List a -> Type where
SNil  :: SList 'Nil
SCons :: Sing x -> SList xs -> SList ('Cons x xs)

type instance Sing = SList

instance SingKind k => SingKind (List k) where
type Demote (List k) = List (Demote k)
fromSing :: Sing (a :: List k) -> List (Demote k)
toSing :: List (Demote k) -> SomeSing (List k)
``````

This definition of `toSing` works fine if I pattern-match `x` and `xs` via a case-of:

``````toSing (Cons x xs) = case toSing x of
SomeSing singX -> case toSing xs of
SomeSing singXs -> SomeSing \$ SCons singX singXs
``````

But it fails if I pattern match via let:

``````toSing (Cons x xs) =
let SomeSing singX = toSing x
SomeSing singXs = toSing xs
in  SomeSing \$ SCons singX singXs
``````

This is the error (another similar one is shown for the following line):

``````error:
• Couldn't match type ‘x0’ with ‘a’
Expected: Sing @k x0
Actual: Sing @k1 a
• because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor:
SomeSing :: forall k (a :: k). Sing a -> SomeSing k,
in a pattern binding
at door.hs:169:13-26
• In the pattern: SomeSing singX
In a pattern binding: SomeSing singX = toSing x
In the expression:
let
SomeSing singX = toSing x
SomeSing singXs = toSing xs
in SomeSing \$ SCons singX singXs
• Relevant bindings include
singXs :: SList xs0 (bound at door.hs:170:22)
xs :: List (Demote k1) (bound at door.hs:168:20)
x :: Demote k1 (bound at door.hs:168:18)
toSing :: List (Demote k1) -> SomeSing (List k1)
(bound at door.hs:167:5)
|
|         let SomeSing singX = toSing x
|                      ^^^^^
``````

Can you explain why let bindings behave differently from a case-of and in this case they fail?

Solution

• `singX` will have a different type, depending on the value of `x`, namely, the specific singleton type corresponding to that value. That means also that the `SCons singX singXs` expression has a different type in each case. None of this is really allowed in Haskell, it's not a dependently-typed language after all.

It is ok for the RHS of a `case` or function clause to be polymorphic, and then be instantiated to the suitable type at the point when the runtime commits to that clause. That does however require clearly delimiting the scope wherein this type variable is polymorphic. A `case` statement does this, a `let` would not, so it's not possible to do it this way.