bug. probably in code with a type error.

[sweirich]

ghc-stage2: panic! (the 'impossible' happened) (GHC version 7.11.20150420 for x86_64-apple-darwin): ds_co_binds EvBindsVar

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

module Part5 where

import Prelude ( Bool(..), undefined, return ) import GHC.TypeLits ( type (-) ) import Data.Type.Equality import GHC.Exts import Data.Type.Bool import Data.Proxy

data Univ = U | K * | I

-- standard definition of natural numbers and their -- singletons data Nat :: * where Zero :: Nat Succ :: Nat -> Nat

data family Sing (a :: k)

data instance Sing (n :: Nat) where SZero :: Sing 'Zero SSucc :: Sing n -> Sing ('Succ n)

data instance Sing (t :: *) where SNat :: Sing Nat SBool :: Sing Bool

(+) :: Nat -> Nat -> Nat Zero + m = m Succ n + m = Succ (n + m) infixl 6 +

type family a :+ b where 'Zero :+ m = m 'Succ n :+ m = 'Succ (n :+ m)

(%:+) :: Sing a -> Sing b -> Sing (a :+ b) SZero %:+ m = m SSucc n %:+ m = SSucc (n %:+ m)

-- standard singletons for lists and booleans data instance Sing (a :: [k]) where SNil :: Sing '[] SCons :: Sing h -> Sing t -> Sing (h ': t) infixr 5 SCons

data instance Sing (a :: Bool) where SFalse :: Sing 'False STrue :: Sing 'True

-- If type family from Data.Type.Bool sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c) sIf SFalse c = c sIf STrue b = b

-- The actual start of the example

-- being Haskell, we'll index our expression type -- by ACTUAL types.

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

data instance Sing (e :: Expr 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)

type SExpr (e :: Expr t) = Sing e

eval :: Expr 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

type family Eval (x :: Expr 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)

sEval :: SExpr 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)

-- Plan: Index by final and initial stack configuration

-- a heterogenously-type indexed relation type Rel = forall (ti :: ) (tj :: ). ti -> tj -> *

data List (x :: Rel) :: Rel where Nil :: List x i i (:::) :: forall (x :: Rel) (ti :: ) (tj :: ) (tk :: *) (i :: ti) (j :: tj) (k :: tk) . x i j -> List x j k -> List x i k infixr 5 :::

(++) :: List x i j -> List x j k -> List x i k Nil ++ ys = ys (x ::: xs) ++ ys = x ::: (xs ++ ys) infixr 5 ++