Polymorphic result type GADT function

Question

In the following code, what can I replace x = .... Note that I don't want to put a class restriction on a (of course, a is of kind Bool already anyway so can only take one of two types).

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: D a
x = ...

Basically, with GADTs like this it's easy to do polymorphism on the input (just match on the appropriate constructors) but I want to use polymorphism in the output.

Answer 1

This requires dependent types - there is no way around it. In Idris, a Haskell-like dependently typed language you can write this just fine:

data D : Bool -> Type where
  D1 : D True
  D2 : D False

-- The `{ .. }` mean the argument is inferred.
x : {a : Bool} -> D a
x {a = True} = D1
x {a = False} = D2

In Haskell, the only way you can dispatch based on type at runtime is through type classes, so you need a constraint. In fact, as @András points out there is SingI that is made for this (it comes from a package singletons which deals exactly with this sort of problem).

In your case, that would be:

{-# LANGUAGE GADTs, TypeInType, ScopedTypeVariables #-}

import Data.Singletons.Prelude   

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: forall a. SingI a => D a
x = case sing :: Sing a of
      STrue -> D1
      SFalse -> D2

It might be worth mentioning that although there is a SingI constraint, it has all of the appropriate instances already defined with it. Anything else that is a valid D type but not with a Bool argument (like D Any) fails at compile time (there is simply no SingI instance found).

ghci> let _ = x :: D True
ghci> let _ = x :: D False
ghci> let _ = x :: D Any
<interactive> error:
  • No instance for (SingI Any) arising from a use of ‘x’
  • In the expression: x :: D Any
    In a pattern binding: _ = x :: D Any