#13953: forall -------------------------------------+------------------------------------- Reporter: zaoqi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Keywords: forall | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs --Copyright (C) 2017 Zaoqi --This program is free software: you can redistribute it and/or modify --it under the terms of the GNU Affero General Public License as published --by the Free Software Foundation, either version 3 of the License, or --(at your option) any later version. --This program is distributed in the hope that it will be useful, --but WITHOUT ANY WARRANTY; without even the implied warranty of --MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the --GNU Affero General Public License for more details. --You should have received a copy of the GNU Affero General Public License --along with this program. If not, see http://www.gnu.org/licenses/. {-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes, UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction, ScopedTypeVariables #-} module Data.U where data U :: [*] -> * where UOne :: x -> U (x : xs) USucc :: U xs -> U (x : xs) class Usuccs a b where usuccs :: U a -> U b instance Usuccs a a where usuccs = id instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where usuccs (UOne x) = UOne x usuccs (USucc xs) = USucc (usuccs xs) instance Usuccs xs (x : xs) where usuccs = USucc instance Usuccs xs ys => Usuccs xs (y : ys) where usuccs x = USucc (usuccs x) u :: forall x xs. Usuccs '[x] xs => x -> U xs u x = usuccs (UOne x :: U '[x]) class T a b where t :: U a -> U b instance Usuccs '[x] t => T '[x] t where t (UOne x) = u x instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where t (UOne x) = u x t (USucc xs) = t xs instance Eq x => Eq (U '[x]) where UOne x == UOne y = x == y instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where UOne x == UOne y = x == y USucc xs == USucc ys = xs == ys _ == _ = False instance Show x => Show (U '[x]) where show (UOne x) = "(u " ++ showsPrec 11 x ")" instance (Show x, Show (U xs)) => Show (U (x : xs)) where show (UOne x) = "(u " ++ showsPrec 11 x ")" show (USucc xs) = show xs }}} {{{ GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Prelude> :load U.hs [1 of 1] Compiling Data.U ( U.hs, interpreted ) Ok, modules loaded: Data.U. *Data.U> :t u u :: Usuccs '[x] xs => x -> U xs }}} ------------------------------------------------------ {{{#!hs --Copyright (C) 2017 Zaoqi --This program is free software: you can redistribute it and/or modify --it under the terms of the GNU Affero General Public License as published --by the Free Software Foundation, either version 3 of the License, or --(at your option) any later version. --This program is distributed in the hope that it will be useful, --but WITHOUT ANY WARRANTY; without even the implied warranty of --MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the --GNU Affero General Public License for more details. --You should have received a copy of the GNU Affero General Public License --along with this program. If not, see http://www.gnu.org/licenses/. {-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes, UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction, ScopedTypeVariables #-} module Data.U where data U :: [*] -> * where UOne :: x -> U (x : xs) USucc :: U xs -> U (x : xs) class Usuccs a b where usuccs :: U a -> U b instance Usuccs a a where usuccs = id instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where usuccs (UOne x) = UOne x usuccs (USucc xs) = USucc (usuccs xs) instance Usuccs xs (x : xs) where usuccs = USucc instance Usuccs xs ys => Usuccs xs (y : ys) where usuccs x = USucc (usuccs x) u :: Usuccs '[x] xs => x -> U xs u x = usuccs (UOne x :: U '[x]) class T a b where t :: U a -> U b instance Usuccs '[x] t => T '[x] t where t (UOne x) = u x instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where t (UOne x) = u x t (USucc xs) = t xs instance Eq x => Eq (U '[x]) where UOne x == UOne y = x == y instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where UOne x == UOne y = x == y USucc xs == USucc ys = xs == ys _ == _ = False instance Show x => Show (U '[x]) where show (UOne x) = "(u " ++ showsPrec 11 x ")" instance (Show x, Show (U xs)) => Show (U (x : xs)) where show (UOne x) = "(u " ++ showsPrec 11 x ")" show (USucc xs) = show xs }}} {{{ GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Prelude> :load U.hs [1 of 1] Compiling Data.U ( U.hs, interpreted ) U.hs:39:7: error: • Could not deduce (Usuccs '[x0] xs) arising from a use of ‘usuccs’ from the context: Usuccs '[x] xs bound by the type signature for: u :: Usuccs '[x] xs => x -> U xs at U.hs:38:1-32 The type variable ‘x0’ is ambiguous Relevant bindings include u :: x -> U xs (bound at U.hs:39:1) • In the expression: usuccs (UOne x :: U '[x]) In an equation for ‘u’: u x = usuccs (UOne x :: U '[x]) U.hs:39:15: error: • Couldn't match type ‘x’ with ‘x1’ ‘x’ is a rigid type variable bound by the type signature for: u :: forall x (xs :: [*]). Usuccs '[x] xs => x -> U xs at U.hs:38:6 ‘x1’ is a rigid type variable bound by an expression type signature: forall x1. U '[x1] at U.hs:39:25 Expected type: U '[x1] Actual type: U '[x] • In the first argument of ‘usuccs’, namely ‘(UOne x :: U '[x])’ In the expression: usuccs (UOne x :: U '[x]) In an equation for ‘u’: u x = usuccs (UOne x :: U '[x]) • Relevant bindings include x :: x (bound at U.hs:39:3) u :: x -> U xs (bound at U.hs:39:1) Failed, modules loaded: none. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13953 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler