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

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?

CodePudding user response：

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.