CODEWITHSUNDEEP
haskelltypes
ntc2
ntc2

Reputation: 11912

How to safely case on kind-constrained type variable in Haskell?

Question

I want to case on a type variable that is restricted to finitely many possibilities due to a kind constraint. And I want to know statically that casing will always discover one of these finitely many possibilities. I can't figure out how to write this case without an unreachable catch-all.

As a concrete example, suppose I have a data kind

data{-kind-} Temp = Hot | Cold

Then my goal is write a function like caseTemp below that determines the Temp a given Temp-kinded type. Something like

data CaseTemp (t :: Temp) where
  IsHot :: CaseTemp 'Hot
  IsCold :: CaseTemp 'Cold

caseTemp :: forall (t :: Temp). CaseTemp t
caseTemp = ???

I'm OK with having some extra constraints on caseTemp, like the Typeable t in my failed attempt below. Or even with an entirely different approach.

Failed Solution Attempt

Here is my best attempt, but it includes a branch that I think should be unreachable, and that would allow caseTemp to break silently if I added another constructor to Temp (tested in GHC 8.0.2):

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
module SOQuestion where

import Data.Typeable ( (:~:)(..), Typeable, eqT )

data{-kind-} Temp = Hot | Cold

data CaseTemp (t :: Temp) where
  IsHot :: CaseTemp 'Hot
  IsCold :: CaseTemp 'Cold
deriving instance Show (CaseTemp t)

caseTemp :: forall (t :: Temp). Typeable t => CaseTemp t
caseTemp =
  case eqT :: Maybe (t :~: 'Hot) of
    Just Refl -> IsHot
    Nothing -> case eqT :: Maybe (t :~: 'Cold) of
                 -- (GHC says this "pattern match is redundant" ???
                 -- Sounds like a bug!)
                 Just Refl -> IsCold
                 -- MY QUESTION: is there a way to eliminate the
                 -- unreachable branch here?
                 Nothing -> error "Unreachable!"

The problem with this attempt is that GHC believes the Nothing -> error "Unreachable!" branch is reachable.

Updates

User @Alec mentions that Any :: Temp is a fundamental reason that it's impossible to do what I want, since e.g.

import GHC.Prim ( Any )
[...]
badCase :: CaseTemp Any
badCase = undefined :: CaseTemp Any

is accepted by GHC. However, Any is not Typeable, so it's not clear to me that putting constraints on caseTemp couldn't work around this.

Upvotes: 0

Views: 97

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

There isn't a direct way, because when eqT returns Nothing it doesn't come with a disequality proof.

How about using a type class?

class IsTemp (b :: Temp) where
  caseTemp :: CaseTemp b

Upvotes: 2

Related Questions