Re: [GHC] #14203: GHC-inferred type signature doesn't actually typecheck

12 Sep 2017

      #14203: GHC-inferred type signature doesn't actually typecheck
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Huh, that's interesting... how do you resolve such an ambiguity, then?
 Normally, my approach is to add proxies until the ambiguity is resolved,
 such as what I tried below:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data TyFun :: * -> * -> *
 type a ~> b = TyFun a b -> *
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 data family Sing :: k -> *

 data Sigma (a :: *) :: (a ~> *) -> * where
   MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
              Sing x -> Apply p x -> Sigma a p

 data instance Sing (z :: Sigma a p) where
   SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply
 p x).
               Proxy a -> Proxy p -> Proxy x
            -> Sing sx -> Sing px -> Sing (MkSigma sx px)
 }}}

 But that still results in the same error. Adding `AllowAmbiguousTypes`
 doesn't help either.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:5
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler