Skip to content

Problem with GADTs and explicit type signatures

{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module Main where

data Exp a where
    Val :: a -> Exp b
    App :: Exp a -> Exp b

instance Show (Exp a) where
    show (Val _) = "Val"
    show (App _) = "App"

class LiftToExp a b where
    liftToExp :: a -> Exp b

instance LiftToExp (Exp a) a where
    liftToExp = id

instance Floating a => LiftToExp a b where
    liftToExp v = Val v :: Exp b

{-
Uncommenting the type signature below causes GHCi to fail to load the file:

Test.hs:48:15: error:
    • Overlapping instances for LiftToExp a a0
        arising from a use of ‘liftToExp’
      Matching givens (or their superclasses):
        LiftToExp a a1
          bound by the type signature for:
                     test :: LiftToExp a a1 => a -> Exp b
          at Test.hs:47:1-38
      Matching instances:
        instance LiftToExp a b -- Defined at Test.hs:22:10
        instance LiftToExp (Exp a) a -- Defined at Test.hs:19:10
      (The choice depends on the instantiation of ‘a, a0’)
    • In the first argument of ‘App’, namely ‘(liftToExp x)’
      In the expression: App (liftToExp x)
      In an equation for ‘test’: test x = App (liftToExp x)

However typing :t test at the GHCi prompt gives this exact signature.
-}

--test :: (LiftToExp a a1) => a -> Exp b
test x = App (liftToExp x)

main = putStrLn $ show (test (3.0::Float)::Exp Int)
Edited by Thomas Miedema
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information