Impossible Sat instance

[GoogleCodeExporter]

[Reported by Tillmann Rendel]

Hi again,

unfortunately, the version with nested quotes via type-level naturals does not
work out for me (GHC 7.0.3). The attached code leads to a non-terminating
type-level computation, where Alpha (T (S ... (S a) ... )) is considered for
more and more S. Maybe somehow related to the reification of the Alpha
dictionaries?

(I am also not sure how to define the Subst instance for T, but I would have
figured something out, I guess).

  Tillmann

[-- Attachment #2: staging.lhs --]
[-- Type: text/plain, Encoding: 7bit, Size: 0.6K --]

> {-# LANGUAGE TemplateHaskell
>            , UndecidableInstances
>            , ScopedTypeVariables
>            , FlexibleInstances
>            , MultiParamTypeClasses
>            , GADTs
>            , StandaloneDeriving
>            , Rank2Types
>   #-}
>
> module UnboundStaged where
>
> import Unbound.LocallyNameless

> data Z
> data S n
>
> type N a = Name (T a)
>
> data T a where
>   App :: T a -> T a -> T a
>   Lam :: Bind (N a) (T a) -> T a
>   Var :: N a -> T a
>   Quo :: T (S n) -> T n
>   Spl :: T n -> T (S n)
> deriving instance Show (T a)

> instance Rep a => Alpha (T a)
>

This seems to be a bug in GHC 7.0.x (the 7.0 series had several bugs
relating to inferring dictionaries).  Under GHC 7.2.1 the code
compiles fine.  Unfortunately, it seems it also tickles a bug in our
code to support GADTs:

    *UnboundStaged> fv ((Quo (lam "x" (Spl (var "x")))) :: T Z) :: [N Z]
    *** Exception: Impossible Sat instance!

Original issue reported on code.google.com by byor...@gmail.com on 19 Sep 2012 at 4:09