GHC compiler error

[sweirich]

Exception: compiler/typecheck/TcTyClsDecls.hs:(1377,5)-(1379,67): Irrefutable pattern failed for pattern Just (subst, _)

[sweirich]

{-# LANGUAGE GADTs, PolyKinds, TypeOperators, TemplateHaskell,
             DataKinds, TypeFamilies, UndecidableInstances,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             FlexibleInstances #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors -fprint-explicit-kinds #-}

module Wg28 where

{-

   Towards Dependently-typed Haskell 

   joint work with Richard Eisenberg

   this code requires Richard's fork of GHC

   https://github.com/goldfirere/ghc

-}

import Data.Type.Equality 
import GHC.Exts
import Data.Type.Bool
import Data.Proxy
import Singletons
import GHC.TypeLits

-- Old and (somewhat) boring

data Expr :: * -> * -> * where
  Val  :: t -> Expr a t
  Plus :: Expr a a -> Expr a a -> Expr a a 
  Cond :: Expr a Bool -> Expr a t -> Expr a t -> Expr a t

eval :: Expr Integer t -> t
eval (Val n)        = n
eval (e1 `Plus` e2) = eval e1 + eval e2
eval (Cond e0 e1 e2)  = if eval e0 then eval e1 else eval e2

-- constant folding function. GADT tells us that it preserves types.
optimize :: Expr Integer t -> Expr Integer t
optimize (Val x) = Val x
optimize (Plus (Val 0) e) = optimize e
optimize (Plus e (Val 0)) = optimize e
optimize (Plus e1 e2) = Plus (optimize e1) (optimize e2)
optimize (Cond (Val True) e1 e2) = optimize e1
optimize (Cond (Val False) e1 e2) = optimize e2
optimize (Cond e1 e2 e3) = Cond (optimize e1) (optimize e2) (optimize e3)

-- New! Improved!  (Type family for a promoted GADT)

type family Eval (x :: Expr Nat t) :: t where
  Eval ('Val n) = n
  Eval ('Plus e1 e2) = Eval e1 + Eval e2
  Eval ('Cond e0 e1 e2) = If (Eval e0) (Eval e1) (Eval e2)

-- a Singleton for that GADT (i.e. a GADT indexed by a GADT)

data instance Sing (e :: Expr Nat t) where
  SVal  :: Sing t -> Sing ('Val t)
  SPlus :: Sing a -> Sing b -> Sing ('Plus a b)
  SCond :: Sing b -> Sing t -> Sing f -> Sing ('Cond b t f)

sEval :: Sing e -> Sing (Eval e)
sEval (SVal n) = n
sEval (e1 `SPlus` e2) = (sEval e1) %:+ (sEval e2)
sEval (SCond e0 e1 e2) = sIf (sEval e0) (sEval e1) (sEval e2)                                                 

data Equivalent e where
  Result :: Sing e' -> (Eval e :~: Eval e') -> Equivalent e

lemma :: Proxy n -> (n + 0) :~: n   
lemma _ = Refl

{-                    
lemma SZero = Refl
lemma (SSucc x) = case lemma x of
  Refl -> Refl
-}

sOpt :: Sing e -> Equivalent e
sOpt (SVal x) = Result (SVal x) Refl
sOpt (SPlus (SVal 0) se) = case sOpt se of
  Result se' Refl -> Result se' Refl
-- this lemma is super annoying  
sOpt (SPlus se (SVal 0)) = case (sOpt se) of
  (Result se' Refl) -> case lemma (sEval se') of
                          Refl -> Result se' Refl
sOpt (SPlus e0 e1) = case (sOpt e0, sOpt e1) of
   (Result e0' Refl, Result e1' Refl) -> Result (SPlus e0' e1') Refl

sOpt (SCond (SVal STrue)  e1 e2) = Result e1 Refl
sOpt (SCond (SVal SFalse) e1 e2) = Result e2 Refl
sOpt (SCond e0 e1 e2) = case (sOpt e0, sOpt e1, sOpt e2) of
  (Result e0' Refl, Result e1' Refl, Result e2' Refl) -> Result (SCond e0' e1' e2') Refl

[sweirich]

Also note that the Integer/Nat distinction from TypeLits is REALLY annoying.

[goldfirere]

That error happens when a GADT return type has the wrong shape for your datatype. And I know that GHC panics there -- it's a surprisingly very nasty bug to fix.

[goldfirere]

And, yes, about the Integer/Nat distinction. My thought on that is to make type-level numbers overloaded just like term-level ones. (That could totally happen without kind equalities, of course.)

[sweirich]

It's coming from this decl:

data instance Sing (e :: Expr Nat t) where SVal :: Sing t -> Sing ('Val t) SPlus :: Sing a -> Sing b -> Sing ('Plus a b) SCond :: Sing b -> Sing t -> Sing f -> Sing ('Cond b t f)

[sweirich]

Note how my expr datatype has an extra parameter so that numbers can be Integers in expressions and Nats in types.

[goldfirere]

Add a type annotation somewhere to fix the first parameter to Expr to be Nat. Simon and I went around about this a while ago, but eventually he came up with a good reason that the template for a data family instance shouldn't influence kind-checking the constructor types. So your result types have a more general kind than GHC expects.