{"action":"opened","issue":{"url":"https://api.github.com/repos/goldfirere/ghc/issues/17","labels_url":"https://api.github.com/repos/goldfirere/ghc/issues/17/labels{/name}","comments_url":"https://api.github.com/repos/goldfirere/ghc/issues/17/comments","events_url":"https://api.github.com/repos/goldfirere/ghc/issues/17/events","html_url":"https://github.com/goldfirere/ghc/issues/17","id":76176973,"number":17,"title":"bug. probably in code with a type error. ","user":{"login":"sweirich","id":2103670,"avatar_url":"https://avatars.githubusercontent.com/u/2103670?v=3","gravatar_id":"","url":"https://api.github.com/users/sweirich","html_url":"https://github.com/sweirich","followers_url":"https://api.github.com/users/sweirich/followers","following_url":"https://api.github.com/users/sweirich/following{/other_user}","gists_url":"https://api.github.com/users/sweirich/gists{/gist_id}","starred_url":"https://api.github.com/users/sweirich/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sweirich/subscriptions","organizations_url":"https://api.github.com/users/sweirich/orgs","repos_url":"https://api.github.com/users/sweirich/repos","events_url":"https://api.github.com/users/sweirich/events{/privacy}","received_events_url":"https://api.github.com/users/sweirich/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-05-14T00:33:17Z","updated_at":"2015-05-14T00:33:17Z","closed_at":null,"body":"ghc-stage2: panic! (the 'impossible' happened)   (GHC version 7.11.20150420 for x86_64-apple-darwin): \tds_co_binds EvBindsVar<a3PF>\r\n\r\n\r\n{-# LANGUAGE GADTs, PolyKinds, TypeOperators, TemplateHaskell,\r\n             DataKinds, TypeFamilies, UndecidableInstances,\r\n             FlexibleContexts, RankNTypes, ScopedTypeVariables,\r\n             FlexibleInstances #-}\r\n{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}\r\n\r\nmodule Part5 where\r\n\r\nimport Prelude ( Bool(..), undefined, return )\r\nimport GHC.TypeLits ( type (-) )\r\nimport Data.Type.Equality\r\nimport GHC.Exts\r\nimport Data.Type.Bool\r\nimport Data.Proxy\r\n\r\n\r\ndata Univ = U | K * | I\r\n\r\n-- standard definition of natural numbers and their\r\n-- singletons\r\ndata Nat :: * where\r\n  Zero :: Nat\r\n  Succ :: Nat -> Nat\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (n :: Nat) where\r\n  SZero :: Sing 'Zero\r\n  SSucc :: Sing n -> Sing ('Succ n)\r\n\r\ndata instance Sing (t :: *) where\r\n  SNat  :: Sing Nat\r\n  SBool :: Sing Bool\r\n\r\n(+) :: Nat -> Nat -> Nat\r\nZero   + m = m\r\nSucc n + m = Succ (n + m)\r\ninfixl 6 +\r\n\r\ntype family a :+ b where\r\n  'Zero :+ m = m\r\n  'Succ n :+ m = 'Succ (n :+ m)\r\n\r\n(%:+) :: Sing a -> Sing b -> Sing (a :+ b)\r\nSZero %:+ m = m\r\nSSucc n %:+ m = SSucc (n %:+ m)\r\n\r\n-- standard singletons for lists and booleans\r\ndata instance Sing (a :: [k]) where\r\n  SNil  :: Sing '[]\r\n  SCons :: Sing h -> Sing t -> Sing (h ': t)\r\ninfixr 5 `SCons`\r\n\r\ndata instance Sing (a :: Bool) where\r\n  SFalse :: Sing 'False\r\n  STrue :: Sing 'True\r\n\r\n-- If type family from Data.Type.Bool\r\nsIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)\r\nsIf SFalse _ c = c\r\nsIf STrue  b _ = b\r\n\r\n\r\n-- The actual start of the example\r\n\r\n-- being Haskell, we'll index our expression type\r\n-- by ACTUAL types. \r\n\r\ndata Expr :: * -> * where\r\n  Val  :: t -> Expr t\r\n  Plus :: Expr Nat -> Expr Nat -> Expr Nat\r\n  Cond   :: Expr Bool -> Expr t -> Expr t -> Expr t\r\n\r\ndata instance Sing (e :: Expr t) where\r\n  SVal  :: Sing t -> Sing ('Val t)\r\n  SPlus :: Sing a -> Sing b -> Sing ('Plus a b)\r\n  SCond   :: Sing b -> Sing t -> Sing f -> Sing ('Cond b t f)\r\n\r\ntype SExpr (e :: Expr t) = Sing e\r\n\r\neval :: Expr t -> t\r\neval (Val n)        = n\r\neval (e1 `Plus` e2) = eval e1 + eval e2\r\neval (Cond e0 e1 e2)  = if eval e0 then eval e1 else eval e2\r\n\r\ntype family Eval (x :: Expr t) :: t where\r\n  Eval ('Val n) = n\r\n  Eval ('Plus e1 e2) = Eval e1 :+ Eval e2\r\n  Eval ('Cond e0 e1 e2) = If (Eval e0) (Eval e1) (Eval e2)\r\n\r\nsEval :: SExpr e -> Sing (Eval e)\r\nsEval (SVal n) = n\r\nsEval (e1 `SPlus` e2) = sEval e1 %:+ sEval e2\r\nsEval (SCond e0 e1 e2) = sIf (sEval e0) (sEval e1) (sEval e2)\r\n\r\n-- Plan: Index by final and initial stack configuration\r\n\r\n-- a heterogenously-type indexed relation\r\ntype Rel = forall (ti :: *) (tj :: *). ti -> tj -> *\r\n\r\ndata List (x :: Rel) :: Rel where\r\n  Nil   :: List x i i\r\n  (:::) :: forall (x :: Rel) (ti :: *) (tj :: *) (tk :: *) (i :: ti) (j :: tj) (k :: tk) .\r\n             x i j -> List x j k -> List x i k\r\ninfixr 5 :::\r\n\r\n(++) :: List x i j -> List x j k -> List x i k \r\nNil ++ ys = ys\r\n(x ::: xs) ++ ys = x ::: (xs ++ ys)\r\ninfixr 5 ++\r\n"}}