Re: [Haskell-cafe] Strange "ambiguity" problems thanks to GADTs

27 Jul 2015


      I take back my claim that this is the show/read ambiguity. Alex's recent explanation looks spot on to me.

Richard

On Jul 22, 2015, at 3:53 AM, Oleg Grenrus  wrote:
...
Nailing down `abt` and `abt’`, but keeping `a` free makes the trick:
{-# LANGUAGE DataKinds, PolyKinds, GADTs, RankNTypes, ScopedTypeVariables #-}
data Type = Fun Type Type | Unit
data Sing :: Type -> * where
      SUnit :: Sing Unit
      SFun  :: Sing i -> Sing j -> Sing (Fun i j)
data AST :: (Type -> *) -> Type -> * where
      TT :: AST ast Unit
      App :: ast (Fun a b) -> ast a -> AST ast b
class ABT (abt :: Type -> *) where
      view   :: abt a -> AST abt a
      unview :: AST abt a -> abt a
class WellTypedABT (abt :: Type -> *) where
      unviewWT :: Sing a -> AST abt a -> abt a
      typeOf   :: abt a -> Sing a
type TypeCheckMonad = Maybe
inferType
      :: forall abt abt' a. (ABT abt, WellTypedABT abt')
      => abt a
      -> TypeCheckMonad (abt' a)
   inferType e0 = go e0
     -- b is free, abt and abt' are bounded, class dictionaries come from above.
     where go :: forall b. abt b -> TypeCheckMonad (abt' b)
           go e0' = case view e0' of
                      TT -> return . unviewWT SUnit $ TT
                      App e1 e2 -> do
                      e1' <- go e1
                      case typeOf e1' of
                        -- -Wall doesn't warn about missing SUnit case here, victory!
                        SFun _typ2 typ3 -> do
                          e2' <- inferType e2
                          return . unviewWT typ3 $ App e1' e2'
...
On 07 Jul 2015, at 19:05, wren romano  wrote:
On Tue, Jul 7, 2015 at 3:35 AM, Simon Peyton Jones
 wrote:
...
If you post a repro case someone (even me) might help. The devil is always in the details.
The smallest repro I can come up with (which is still related to the
actual problem) is as follows. In case it matters for the solution,
there are a number of important bits I've erased. Most importantly,
the inferType function is actually mutually recursive with a checkType
function, though that doesn't seem to be the cause of the problem.
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}
data Type = Fun Type Type
data Sing :: Type -> * where
  SFun :: Sing i -> Sing j -> Sing (Fun i j)
data AST :: (Type -> *) -> Type -> * where
  App :: ast (Fun a b) -> ast a -> AST ast b
class ABT (abt :: Type -> *) where
  view   :: abt a -> AST abt a
  unview :: AST abt a -> abt a
class WellTypedABT (abt :: Type -> *) where
  unviewWT :: Sing a -> AST abt a -> abt a
  typeOf   :: abt a -> Sing a
data TypeCheckMonad a = TCM { unTCM :: a }
instance Functor TypeCheckMonad where
  fmap f = TCM . f . unTCM
instance Applicative TypeCheckMonad where
  pure = TCM
  TCM f <*> TCM x = TCM (f x)
instance Monad TypeCheckMonad where
  return      = pure
  TCM x >>= k = k x
inferType
  :: (ABT abt, WellTypedABT abt')
  => abt a
  -> TypeCheckMonad (abt' a)
inferType e0 =
  case view e0 of
  App e1 e2 -> do
      e1' <- inferType e1
      case typeOf e1' of
          SFun typ2 typ3 -> do
              e2' <- inferType e2
              return . unviewWT typ3 $ App e1' e2'
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Strange "ambiguity" problems thanks to GADTs

Richard Eisenberg